LQGStructure
plain-language theorem explainer
LQGStructure enumerates the five canonical structures of loop quantum gravity as an inductive type equipped with a Fintype instance. A researcher connecting loop quantum gravity to Recognition Science would cite it when identifying the configuration space dimension with D+2 for spatial dimension three. The definition is a direct enumeration of the five constructors that automatically derives decidable equality and finite cardinality.
Claim. The set of canonical loop quantum gravity structures consists of the spin network, spin foam, kinematic Hilbert space, Thiemann quantization, and coherent states.
background
Loop quantum gravity quantizes spacetime via spin networks whose edges carry half-integer representation labels j. Recognition Science maps these labels to recognition rungs on the phi-ladder and identifies the five listed structures with the configuration dimension formula D+2. The module states that five structures equal configDim D=5, with the same relation 5=D+2 that appears in the forcing chain for spatial dimension three.
proof idea
This is an enumerative inductive definition whose five constructors automatically derive the Fintype instance, allowing downstream cardinality statements to be discharged by the decide tactic.
why it matters
The definition supplies the finite set whose cardinality is proved equal to 5 and to 3+2 in the downstream results lqgStructureCount and lqg_five_Dp2. It realizes the Recognition Science identification of LQG structures with the D+2 configuration dimension from T8, closing the mapping from spin networks to recognition rungs without axioms or sorrys.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.