LQGCert
plain-language theorem explainer
LQGCert packages two cardinality assertions on the inductive type of LQG structures, confirming exactly five elements and the equality to three plus two. Quantum gravity researchers would cite it to align the canonical spin-network structures with the Recognition Science configuration-dimension formula. The definition is a direct structure with two fields that follow immediately from the Fintype instance on the enumerated inductive type.
Claim. A certificate asserting that the finite set of LQG structures has cardinality five and that this cardinality equals three plus two.
background
The module maps loop quantum gravity to Recognition Science by identifying spin-network labels with recognition rungs on the phi-ladder. LQGStructure is the inductive type whose five constructors are spinNetwork, spinFoamLQG, kinematicHilbert, thiemannQuantization and coherentStates, each deriving a Fintype instance. The module document states that these five structures realise configDim D = 5 and satisfy the relation 5 = D + 2, with D = 3 spatial dimensions taken from the forcing-chain step T8.
proof idea
The declaration is a structure definition whose two fields are the assertions Fintype.card LQGStructure = 5 and Fintype.card LQGStructure = 3 + 2. No lemmas or tactics are invoked; the equalities are immediate once the Fintype instance derived on the inductive type is in scope.
why it matters
The structure supplies the witness consumed by the downstream definition lqgCert. It records the five-structure count that the module document equates to the Recognition Science configDim formula, thereby linking LQG to the forcing-chain landmarks T7 (eight-tick octave) and T8 (D = 3). No open scaffolding remains inside the declaration itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.