Develop a no-sorry proof of the five-dimensional Geode value - #81

Open

DomTheDeveloper wants to merge 30 commits into

mainfrom

geode5-formal-proof

Commits on Jul 23, 2026

Add Geode5 CRT certificate proof layer
DomTheDeveloper
committed
0e63ddd
Add exact Geode5 answer certificate
DomTheDeveloper
committed
60f67aa
Add 480-prime Geode5 residue certificate
DomTheDeveloper
committed
5b0251e
Add Geode5 formal proof audit
DomTheDeveloper
committed
3d56771
Document Geode5 formal proof boundary
DomTheDeveloper
committed
31a7e81
Record Geode5 proof status
DomTheDeveloper
committed
7632e65
Trigger Geode5 proof audit on branch pushes
DomTheDeveloper
committed
6271242
Formalize Geode5 symbolic moment recurrence algebra
DomTheDeveloper
committed
8057669
Audit Geode5 symbolic recurrence and CRT layers
DomTheDeveloper
committed
64dd6c1
Add algebraic integral layer for Geode5 moments
DomTheDeveloper
committed
7ec6565
Use qualified Geode5 integral import
DomTheDeveloper
committed
3d79946
Audit Geode5 integral proof layer
DomTheDeveloper
committed
cc5c4fc
Use Formal Conjectures copyright for Geode5 algebra
DomTheDeveloper
committed
618ec18
Use Formal Conjectures copyright for Geode5 CRT layer
DomTheDeveloper
committed
0e46db9
Add exact Geode5 moment recurrence layer
DomTheDeveloper
committed
8426878
Make Geode5 integral coefficient-linear
DomTheDeveloper
committed
9c90ee6
Audit exact Geode5 recurrence layer
DomTheDeveloper
committed
39d7a89
Formalize Geode5 factorial summand reduction
DomTheDeveloper
committed
ac76e35
Add exact Geode5 sparse remainder tables
DomTheDeveloper
committed
1f4a9b8
Split Geode5 sparse remainder certification
DomTheDeveloper
committed
b5055da
Reduce Geode5 integrality to cyclic multinomial divisibility
DomTheDeveloper
committed
d03acb4
Apply audited Geode5 integral fixes
DomTheDeveloper
committed
a7671f7
Prove Geode5 multinomial length divisibility
DomTheDeveloper
committed
a1e962f
Sync kernel-verified Geode5 integral proof
DomTheDeveloper
committed
1033890
Complete the Geode5 hyper-Catalan integrality bridge
DomTheDeveloper
committed
a5f075e
Bridge Geode5 symbolic recurrence to sparse tables
DomTheDeveloper
committed
26a43d5
Bridge the exact Geode5 benchmark definition to rationals
DomTheDeveloper
committed
b99e02c
Sync kernel-verified Geode5 raw recurrence
DomTheDeveloper
committed
3629ede
Use mathlib's multinomial recurrence for Geode5 integrality
DomTheDeveloper
committed
bc9977e
Use the current factorial divisibility theorem
DomTheDeveloper
committed
ca03b71