lqgCert
plain-language theorem explainer
This definition assembles the LQG certificate by directly supplying the two cardinality statements on LQG structures. A quantum gravity researcher would cite it to record that the five canonical structures match the RS configuration dimension formula. The construction is a direct record that assigns the upstream equality theorems to the two fields of the certificate structure.
Claim. The LQG certificate is the structure asserting that the cardinality of the set of canonical LQG structures equals 5 and also equals 3 + 2.
background
In the Recognition Science treatment of loop quantum gravity, spin networks quantise spacetime with edge labels drawn from recognition rungs. The module identifies five canonical structures (spin network, spin foam, kinematic Hilbert space, Thiemann quantisation, coherent states) whose count is required to equal the configuration dimension D + 2. With D = 3 spatial dimensions this yields the numerical target 5. The structure LQGCert packages exactly these two equalities as its fields.
proof idea
The definition constructs the LQGCert instance by assigning the theorem establishing cardinality 5 to the first field and the theorem establishing cardinality 3 + 2 to the second field. Both upstream results are obtained by the decide tactic on finite types.
why it matters
This definition supplies the concrete witness that the five LQG structures align with the RS eight-tick octave and the forced spatial dimension D = 3. It records the match 5 = D + 2 required by the configuration dimension formula and closes the module with zero sorry or axiom. The certificate stands ready for any downstream argument linking LQG to the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.