rs_quantum_gravity_master_partial_one_statement
plain-language theorem explainer
Universal form of the Session-100 partial quantum-gravity master statement: given continuum Regge–EH recovery with contracted Bianchi, unconditional amplitude-linear forcing, and a derived Page curve, the RS master proposition holds with PTA and strong-field distinctness witnesses already installed. Gravity-track auditors cite it for a single closed Prop rather than a curried conditional. Proof is a one-line term reusing the partial conditional theorem.
Claim. For every hypothesis package asserting discrete-to-continuum Regge–Einstein–Hilbert convergence with contracted discrete Bianchi, unconditional amplitude-linear forcing of the channel response, and a dynamical Page-curve derivation, the RS quantum-gravity master statement holds when the PTA stochastic-GW spectrum is witnessed distinct from inflation and strong-field tests are witnessed distinct from GR.
background
The module is Session 100's partial advancement of Track 7.A. Session 97's conditional master theorem took five open-track hypothesis inputs. This module retires two of them structurally: PTA stochastic-GW distinctness from inflation (Track 6.B) and strong-field tests distinct from GR (Track 6.C), via Lean witnesses from the PTA and strong-field structural modules. Three inputs remain.
RegEHContinuumAndBianchi packages the still-open Track 1.B/1.C load-bearing D2 claim: Regge action converges to Einstein–Hilbert with an explicit residual, and the discrete Bianchi identity contracts. AmplitudeLinearForcedUnconditional is Track 2.C/2.D: amplitude-linear forcing of the channel response with the factor-product joint-substrate axiom lifted. PageCurveDerived is Track 3.C: dynamical Page-curve derivation (Page-time $M^3$ scaling is closed; unitary entropy evolution remains open).
The master proposition conjoins T0–T8 forcing, cost uniqueness, Lorentzian $1+3$ signature, the D2 classical-recovery pieces, amplitude linearity with BMV positivity, Hawking temperature in SI units, and the PTA/strong-field distinctness clauses, matching master-plan §4 Track 7.A verbatim.
proof idea
One-line term-mode wrapper. The body is exactly the partial conditional theorem, which already plugs the PTA distinct-from-inflation witness and the strong-field distinct-from-GR witness into the five-slot master proposition. Quantifying the three remaining hypothesis structures over that theorem yields the $\forall$ form. No extra tactics or lemmas fire.
why it matters
Citation-friendly packaging of Session 100's structural closure of Tracks 6.B and 6.C inside the quantum-gravity master statement. No downstream dependents yet; it sits as a terminal packaging theorem for auditors who want the $\forall$-quantified Prop. Discovery is not claimed: three hypothesis inputs remain open (Regge–EH continuum, unconditional amplitude linearity, Page-curve dynamics), plus the master paper, the §7 falsifier register, and the six §8 done-criteria. Per master plan §6 all four must hold for discovery complete. Framework landmarks T0–T8 enter only as conjuncts inside the master Prop; this declaration does not re-prove them.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.