spinFoamModelCount
The theorem establishes that exactly five spin foam models are enumerated in the Recognition Science framework. Researchers deriving quantum gravity path integrals from recognition lattices would cite this count to fix the model dimension at D=5. The proof is a one-line wrapper that invokes the decide tactic on the Fintype instance of the inductive type.
claimThe set of canonical spin foam models has cardinality five: $|$Ponzano-Regge, EPRL, FK, BO, Engle-Livine$| = 5$.
background
The Spin Foam from RS module derives spin foam models as the Freudenthal triangulation of the recognition lattice, with five canonical models (Ponzano-Regge, EPRL, FK, BO, Engle-Livine) corresponding to configDim D=5. SpinFoamModel is the inductive type whose constructors are exactly these five models and which derives DecidableEq, Repr, BEq, and Fintype. The module states that the fundamental amplitude involves the 6j-symbol with dimension 6 = 2D at D=3, and Lean status is zero sorry and zero axiom.
proof idea
The proof is a one-line wrapper that applies the decide tactic, which evaluates the cardinality directly from the Fintype derivation on the inductive type with five constructors.
why it matters in Recognition Science
This theorem supplies the five_models field inside spinFoamCert, which certifies the spin foam construction. It realizes the framework claim that five models align with D=3 spatial dimensions and the 6j-symbol identities (6 = cube faces). It closes the enumeration step linking Recognition Science to path-integral quantum gravity.
scope and limits
- Does not claim these five models exhaust all possible spin foam constructions outside the recognition lattice.
- Does not derive explicit amplitudes or partition functions for the models.
- Does not address generalizations to dimensions other than D=3.
Lean usage
def cert : SpinFoamCert := { five_models := spinFoamModelCount, sixJ_faces := sixJ_eq_cube_faces, sixJ_2D := sixJ_eq_2D }formal statement (Lean)
27theorem spinFoamModelCount : Fintype.card SpinFoamModel = 5 := by decide
proof body
Term-mode proof.
28
29/-- 6j-symbol dimension = 6 = 2D = cube faces. -/