Develop pure-kernel proof of Chomp 10×42 - #80

Open

DomTheDeveloper wants to merge 37 commits into

mainfrom

proof/chomp-10x42-kernel-certificate

Commits on Jul 23, 2026

Add generic kernel-checked game certificate theorem
DomTheDeveloper
committed
4ac1673
Audit generic Chomp kernel certificate theorem
DomTheDeveloper
committed
84e0cda
Audit axioms of generic certificate theorem
DomTheDeveloper
committed
ce8e0ee
Add exact losing-position rank exporter
DomTheDeveloper
committed
8cf79cf
Add shared proof-DAG extractor and feasibility meter
DomTheDeveloper
committed
3795f9c
Measure Chomp kernel proof-DAG feasibility
DomTheDeveloper
committed
c352542
Add reproducible kernel certificate feasibility audit
DomTheDeveloper
committed
d81aa82
Trigger installed Chomp kernel feasibility audit
DomTheDeveloper
committed
a412aca
Keep existing exact audit unchanged
DomTheDeveloper
committed
3ecb3ec
Strengthen finite game certificate with exact closure
DomTheDeveloper
committed
a2f8925
Require closure only where the losing rule needs it
DomTheDeveloper
committed
a541615
Repair rank induction in Chomp kernel certificate
DomTheDeveloper
committed
7e9e7ae
Remove redundant label rewrites in certificate induction
DomTheDeveloper
committed
5ba5a55
Prove every legal Chomp move decreases area
DomTheDeveloper
committed
baa922a
Audit Chomp rank proof against canonical DTD branch
DomTheDeveloper
committed
2da8a4a
Add exact MDD compressor for Chomp P-set
DomTheDeveloper
committed
d1f28c2
Record exact Chomp P-set MDD compression measurement
DomTheDeveloper
committed
785406a
Add kernel theorems for symbolic MDD language certificates
DomTheDeveloper
committed
fda0bea
Audit symbolic MDD certificate theorems
DomTheDeveloper
committed
b418a09
Add generic kernel theorem from a certified P-set
DomTheDeveloper
committed
947a637
Audit certified P-set kernel theorem
DomTheDeveloper
committed
8e47ecc
Prove legal Chomp moves preserve valid positions
DomTheDeveloper
committed
a9405e5
Audit Chomp position-preservation theorems
DomTheDeveloper
committed
bbf2434
Prove totality and exclusivity for ranked normal-play games
DomTheDeveloper
committed
b6f588e
Bridge kernel losing outcomes to catalog P-positions
DomTheDeveloper
committed
4743a85
Audit ranked-game determinacy and catalog bridge
DomTheDeveloper
committed
a5ba846
Use canonical Formal Conjectures imports
DomTheDeveloper
committed
ac5494d
Use canonical Formal Conjectures imports for MDD checker
DomTheDeveloper
committed
c80f98d
Compile Chomp support modules onto Lean import path
DomTheDeveloper
committed
4fedd8f
Emit canonical Chomp catalog olean for support modules
DomTheDeveloper
committed
ba12b9b
Build canonical Formal Conjectures utility library before Chomp audit
DomTheDeveloper
committed
3840e9a
Split zero-row bite Ferrers proof by list shape
DomTheDeveloper
committed
93f0128
ci: run installed Chomp Lean audit
DomTheDeveloper
committed
ba1f9ab
fix: prove concrete Chomp positions explicitly
DomTheDeveloper
committed
a2fbeea
feat: add move-closed local P-set certificates
DomTheDeveloper
committed
3e76292
feat: formalize the finite Chomp certificate domain
DomTheDeveloper
committed
ee3bc2b
feat: expose the final local symbolic-certificate theorem
DomTheDeveloper
committed
ddac23b