SpinFoamCert
plain-language theorem explainer
SpinFoamCert bundles the certification that the Recognition Science spin foam model has exactly five canonical realizations and that the 6j-symbol dimension satisfies both equality to 6 and to twice 3. Quantum gravity researchers using discrete path integrals would reference this to anchor the model count to the Recognition lattice. The declaration consists of a structure definition with three field equalities and no further proof obligations.
Claim. The structure whose fields assert that the set of spin foam models has cardinality 5, that the 6j-symbol dimension equals 6, and that the 6j-symbol dimension equals $2 times 3$.
background
Recognition Science formulates spin foams as the Freudenthal triangulation of the recognition lattice. The module defines SpinFoamModel as the inductive type with constructors PonzanoRegge, EPRL, FK, BO, EngleLivine, which derives Fintype to enable cardinality computation. sixJDimension is defined as the natural number 6, interpreted as the number of faces of the 3-cube and as 2D for spatial dimension D=3.
proof idea
The declaration is a structure definition introducing three fields. It requires no lemmas or tactics; the fields are asserted directly as part of the structure.
why it matters
SpinFoamCert supplies the data instantiated by the downstream spinFoamCert definition. It encodes the framework claim that five models match configDim D=5 and that the 6j dimension is 6=2D, consistent with the forcing chain derivation of three spatial dimensions. This closes the certification for the spin foam path integral in RS without introducing axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.