spinFoamCert
plain-language theorem explainer
The definition constructs an instance of the SpinFoamCert structure by substituting the proved count of five spin foam models together with the two equalities that fix the 6j-symbol dimension at 6 and at twice 3. A researcher working on discrete quantum gravity would cite it to record that the Recognition Science lattice reproduces the canonical five-model count and the cube-face dimension expected for a three-dimensional triangulation. The construction is a direct record instance that applies the three upstream equalities without further steps
Claim. The spin foam certificate is the structure asserting that the cardinality of the set of spin foam models equals 5, the 6j-symbol dimension equals 6, and the 6j-symbol dimension equals $2 times 3$.
background
In the Recognition Science treatment, spin foams arise as the Freudenthal triangulation of the recognition lattice. Five canonical models (Ponzano-Regge, EPRL, FK, BO, Engle-Livine) correspond to configuration dimension D = 5, while the fundamental amplitude employs the 6j-symbol whose dimension is fixed at 6, matching twice the spatial dimension 3 and the number of faces of a cube. The SpinFoamCert structure packages exactly these three assertions: model count equals 5, 6j dimension equals 6, and 6j dimension equals 2 times 3.
proof idea
The definition is a direct structure instance that fills the three fields of SpinFoamCert by substituting the upstream theorems spinFoamModelCount, sixJ_eq_cube_faces, and sixJ_eq_2D. No additional reasoning or tactics are applied beyond the substitution of the already-proved equalities.
why it matters
This definition supplies the concrete certificate that closes the spin foam section of the Recognition Science framework, confirming that the lattice yields the five standard models and the 6j properties required for the path-integral formulation at D = 3. It sits at the interface between the discrete recognition lattice and continuum quantum gravity models, with the upstream equalities (proved by reflexivity and decision) discharging all obligations in the Lean formalization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.