lqg_five_Dp2
plain-language theorem explainer
The theorem asserts that the inductive type of five canonical LQG structures has cardinality exactly five. A researcher checking the Recognition Science dimension relation D + 2 would cite this cardinality when confirming the count of spin-network objects. The proof is a one-line decision procedure that evaluates the Fintype instance directly.
Claim. $|LQGStructure| = 5$, where the five elements are the spin network, spin foam, kinematic Hilbert space, Thiemann quantization, and coherent states, matching the relation $5 = D + 2$ for spatial dimension $D = 3$.
background
The module defines five canonical LQG structures via the inductive type LQGStructure whose constructors are spinNetwork, spinFoamLQG, kinematicHilbert, thiemannQuantization, and coherentStates. Each constructor derives DecidableEq, Repr, BEq, and Fintype, so the type is finite and its cardinality is computable. The surrounding documentation states that these five objects correspond to the configuration dimension formula yielding five when D equals three, and that the same relation 5 = D + 2 appears in the Recognition Science treatment of loop quantum gravity.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the equality Fintype.card LQGStructure = 3 + 2. No lemmas are named; the tactic reduces the finite cardinality computation to a decidable equality on natural numbers.
why it matters
The result supplies the five_Dp2 field of the downstream lqgCert certificate. It thereby confirms the module claim that five LQG structures equal D + 2, consistent with the spatial dimension D = 3 obtained from the forcing chain at T8. The declaration closes a small verification step inside the larger LQG-from-RS correspondence without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.