SpinFoamModel
plain-language theorem explainer
SpinFoamModel enumerates the five standard spin foam models employed in quantum gravity path integrals. Researchers connecting discrete quantum gravity to Recognition Science lattices would cite this enumeration when fixing the configuration dimension to D = 5. The declaration is a direct inductive type with five named constructors and derived decidability and finiteness instances.
Claim. The inductive type of spin foam models is generated by the five constructors Ponzano-Regge, Engle-Pereira-Rovelli-Livine, Freidel-Krasnov, Barrett-O'Raifeartaigh, and Engle-Livine.
background
Spin foam models supply a path-integral formulation of quantum gravity. In Recognition Science the spin foam is identified with the Freudenthal triangulation of the recognition lattice, and the five listed models realize configuration dimension D = 5. The fundamental amplitude is built from the 6j-symbol whose dimension equals 6, which equals twice the spatial dimension D = 3.
proof idea
The declaration is a direct inductive definition that introduces the five constructors and derives DecidableEq, Repr, BEq, and Fintype instances automatically.
why it matters
This definition supplies the finite set required by the SpinFoamCert structure, which records that Fintype.card SpinFoamModel = 5 and that the 6j-symbol dimension equals 6 = 2D. It realizes the module statement that five canonical models equal configDim D = 5, thereby linking the Recognition Science lattice to standard quantum gravity discretizations before the cardinality theorem spinFoamModelCount is proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.