lqgStructureCount
plain-language theorem explainer
The theorem establishes that the set of canonical loop quantum gravity structures derived from Recognition Science has cardinality exactly five. Researchers working on spin-network quantization or RS-to-LQG mappings would cite this count. The proof is a one-line wrapper that invokes the decide tactic on the finite-type cardinality of the inductive enumeration.
Claim. The cardinality of the set of canonical loop quantum gravity structures is five, where the structures are the spin network, spin foam, kinematic Hilbert space, Thiemann quantization, and coherent states.
background
The module derives loop quantum gravity from Recognition Science by identifying spin-network edge labels with recognition rungs on the phi-ladder. Volume eigenvalues are expressed as V = ℓ_P³ × (8πγ)^{3/2} × sqrt(j(j+1)(j+2)) with j corresponding to rung indices. Five canonical structures are enumerated inductively: spin network, spin foam, kinematic Hilbert space, Thiemann quantization, and coherent states. This enumeration satisfies the relation five equals configuration dimension D plus two, with D fixed at three spatial dimensions by the T8 step of the unified forcing chain.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the proposition Fintype.card of the inductive type equals five. The tactic reduces the equality to a decidable computation over the five constructors and confirms it holds by exhaustive enumeration.
why it matters
This cardinality result supplies the five_structures field of the downstream LQG certificate definition, which pairs it with the five-equals-D-plus-two relation. It closes the counting step in the claim that LQG structures match the configuration-dimension formula native to Recognition Science. The count aligns with the eight-tick octave and the T8 forcing of D equals three; no open scaffolding remains in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.