QGApproach
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not derive dynamical equivalence among the five approaches.
- Does not connect the enumeration to the Recognition Composition Law.
- Does not compute explicit numerical values for bounce radii or echo delays.
- Does not extend the list to additional quantum gravity proposals.
formal statement (Lean)
28inductive QGApproach where
29 | canonicalQG | spinFoam | causalSets | CDT | loopQG
30 deriving DecidableEq, Repr, BEq, Fintype
31