Develop pure-kernel proof of Chomp 10×42

[DomTheDeveloper]

Goal

Replace the external-computation boundary in DTD Formal Conjectures PR #185 with genuine Lean proofs that the three displayed children of the 10 × 42 rectangle are losing Chomp positions.

Trust policy

The final development must contain no:

• sorry or admit;
• native_decide;
• custom axioms;
• Lean.ofReduce or Lean.ofReduceBool;
• compiler-trust escape.

External C++ programs may discover or compress certificates, but Lean must verify their mathematical content.

Kernel theorem layers

This branch develops:

• inductive normal-play losing/winning proof objects;
• a ranked-game theorem reconstructing outcomes from an exact finite certificate;
• a generic theorem deriving outcomes from the two P-set laws;
• Chomp area-decrease and position-preservation lemmas;
• deterministic automaton/MDD inclusion and disjointness certificate theorems.

The finite certificate semantics require complete representation of every real child at a losing node. A winning node needs one proved legal losing reply.

Why a raw proof DAG is not viable

A theorem-per-position proof DAG did not close even after 20,000,000 unique nodes and 82,862,247 proof edges for the first target alone. Therefore the final proof cannot replay the search state by state.

Exact symbolic representation

The complete losing-position stream through the third target contains 107,342,138 states. An exact reduced layered multi-valued decision diagram compresses it to:

• 16,906,422 nodes;
• 96,754,877 transitions.

The MDD builder uses hashes only to find candidate buckets; nodes are merged after exact transition comparison. The builder remains untrusted.

Remaining formal obligation

Instantiate the MDD theorem layer with concrete node tables and kernel-checkable local certificates proving, in the finite descendant domain of the three targets:

1. no represented losing position has a represented losing child;
2. every valid represented non-losing position has a legal reply in the losing set;
3. all three target children belong to the losing set;
4. the descendant domain is closed under legal Chomp moves.

The ranked P-set theorem then yields the three losing proofs and removes the final sorry from DTD PR #185.

Canonical staging PR

DomTheDeveloper/formal-conjectures#185

That PR remains draft until the final theorem and axiom audit are green.