RSQuantumGravityMaster
plain-language theorem explainer
The master quantum-gravity claim is the six-sector conjunction (substrate, classical limit, quantum channel, empirical sectors, discriminators, zero free parameters) matching Track 7.A verbatim. Five open-track hypotheses supply the still-open clauses; eight closed clauses sit as named props. Anyone citing the RS gravity discovery cites this statement shape. The body is a pure Prop conjunction, not a proof.
Claim. Given hypotheses that (i) Regge action converges to Einstein–Hilbert with contracted discrete Bianchi, (ii) amplitude response is forced linear without factor-product axioms, (iii) the Page curve is dynamically derived, (iv) the RS PTA stochastic-GW spectrum differs from inflationary $n_t$, and (v) strong-field tests differ from pure GR: the master claim is the conjunction of T0–T8 forcing with cost uniqueness and Lorentzian $1{+}3$ signature; those classical-limit facts; amplitude-linear forcing with unconditional BMV positivity; Hawking temperature in SI, a distinct RS $c$ observable, the Page curve, and $\Omega_\Lambda$ from $\varphi$; QNM distinction from LQG/string, PTA distinction, and strong-field distinction; and zero free parameters in the gravity sector.
background
Track 7.A authors the single master statement of the RS quantum-gravity program. The local module does not claim the discovery is finished; it packages twelve clauses into six done-criteria sectors (D1–D6) so that closed work and open tracks share one Prop.
D1 (substrate) bundles the T0–T8 forcing chain, uniqueness of the J-cost $J(x)=(x+x^{-1})/2-1$, and Lorentzian $1{+}3$ signature. D2 is classical recovery: Regge-to-Einstein–Hilbert continuum limit plus contracted discrete Bianchi (Schläfli), both still open and carried by the first hypothesis structure. D3 is the quantum channel: unconditional amplitude-linear forcing (open lift of a factor-product axiom) conjoined with already-proved BMV positivity. D4–D5 mix closed SI anchors (Hawking temperature, distinct $c$, $\Omega_\Lambda$ from $\varphi$, QNM discriminators) with open Page-curve dynamics, PTA spectrum, and strong-field tests. D6 asserts the gravity sector has zero free parameters.
Spatial dimension $D=3$ enters via the forcing chain (T8) and related constants modules; the statement itself only names the sector props.
proof idea
No proof: this is a definition of a five-argument Prop. The body is a nested conjunction whose six blocks are the D1–D6 sectors. Closed conjuncts appear as bare named props (T0_T8_holds, CostUniqueness, Lorentzian_1_3, bmv_positive_unconditional, Hawking SI, $c$ distinction, $\Omega_\Lambda$ from $\varphi$, QNM distinction, zero free parameters). Open conjuncts are projected fields of the five hypothesis structures (Regge–EH continuum and discrete Bianchi; unconditional amplitude linearity; Page curve; PTA vs inflation; strong field vs GR). Downstream theorems inhabit this Prop by supplying those five structures and discharging the closed conjuncts from Sessions 89–96 anchors.
why it matters
This is the Track 7.A master-plan template made into a Lean Prop: the citation surface for the whole gravity discovery. The conditional theorem rs_quantum_gravity_master_conditional and the $\forall$-form rs_quantum_gravity_master_one_statement prove exactly this Prop under the five open-track inputs, discharging eight closed clauses from existing Lean theorems. Deeper-partial variants reuse the same Prop with some hypotheses replaced by witnesses. Non-circularity audits classify its clauses.
Framework landmarks tied in: T0–T8 substrate forcing (including $D=3$ and the eight-tick octave), J-cost uniqueness (T5), and the zero-parameter gravity sector. The discovery is complete only when Tracks 1.B/1.C, 2.C/2.D unconditional, 3.C, 6.B, and 6.C discharge the five hypothesis structures and an unconditional master theorem (no inputs) can be stated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.