QGApproach
plain-language theorem explainer
QGApproach enumerates the five quantum gravity frameworks recovered by Recognition Science through its bounce-radius construction. Researchers modeling quantum gravity unification cite this list to establish that exactly five standard approaches are subsumed. The declaration is a direct inductive type with five constructors and automatic derivation of Fintype, decidable equality, and related instances.
Claim. Let $Q$ be the finite set whose elements are canonical quantum gravity, spin foam, causal sets, causal dynamical triangulations, and loop quantum gravity.
background
The module develops structural consequences of the Recognition Science bounce radius $r_{min}(N) = ell_P phi^{N/2}$ for rung gap $N$. The module documentation states that five canonical quantum gravity approaches are subsumed by RS under this construction, corresponding to configuration dimension five. This inductive enumeration supplies the finite set whose cardinality and ordering properties are certified in downstream structures.
proof idea
The declaration is the base inductive definition introducing the five constructors; no lemmas or tactics are applied beyond the automatic derivation of Fintype and related type classes.
why it matters
This definition supplies the finite set whose cardinality is established as five in qgApproachCount and which populates the QuantumGravityCert structure asserting positivity of the bounce radius together with monotonicity of echo delays. It directly implements the module claim that RS subsumes the five listed approaches under a single bounce-radius mechanism, consistent with the phi-ladder and eight-tick octave in the Recognition Science forcing chain. No open questions or scaffolding are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.