rs_quantum_gravity_master_partial_conditional
plain-language theorem explainer
Under three remaining structural hypotheses (regularized Einstein–Hilbert continuum plus Bianchi, unconditional amplitude linearity, and a derived Page curve), the Recognition Science quantum-gravity master statement holds when the PTA and strong-field discriminators are the Session-100 algebraic witnesses. Gravity and cosmology workers cite it as the reduced-input form of the master theorem. The proof is a one-line application of the five-input Session-97 conditional with those two witnesses plugged in.
Claim. Assume a regularized Einstein–Hilbert continuum satisfying the Bianchi identities, that amplitude linearity is forced unconditionally, and that the Page curve is derived. Then the RS quantum-gravity master package holds when the PTA stochastic-GW clause is witnessed by the algebraic PTA-versus-inflation discriminator and the strong-field clause is witnessed by the algebraic strong-field-versus-GR discriminator.
background
This module is the Session-100 partial advance of the Gravity master theorem. Session 97 packaged five open tracks as hypothesis inputs to a single conditional master statement. Two of those tracks (PTA stochastic GW distinct from inflation; strong-field tests distinct from GR) now have Lean inhabitants from PTAStochasticGWStructural and StrongFieldStructural.
The PTA witness is an inhabitant of the master-theorem hypothesis type for PTA-versus-inflation distinctness; its doc states it "retires the PTA hypothesis from the conditional master theorem." The strong-field witness plays the analogous role for Track 6.C. Both are theorem-grade algebraically (positivity of $\log\varphi$ and of $\varphi^{-44}$) and remain hypothesis-grade only for dataset match (NANOGrav/EPTA; EHT/GRAVITY/Cassini).
The three still-open inputs are continuum-plus-Bianchi regularization, unconditional amplitude linearity, and Page-curve derivation. RS-native units in the background fix $c=1$ and $\hbar=\varphi^{-5}$, which underwrite the algebraic discriminators.
proof idea
One-line wrapper. Feed the three remaining hypotheses together with the two pre-built witnesses ptaDistinctFromInflationWitness and strongFieldDistinctFromGRWitness into the Session-97 five-input conditional rs_quantum_gravity_master_conditional. No new algebra is proved here; the reduction is purely by supplying inhabitants for the two retired hypothesis slots.
why it matters
This is the Gravity Track 7.A partial master: it cuts the open hypothesis count from five to three without softening the master claim. Downstream, rs_quantum_gravity_master_partial_one_statement rephrases it as a universal quantification over the three remaining inputs, and the module's authorship/status tracker records the Session-100 closure snapshot.
In the broader RS chain it sits after the forcing landmarks (J-uniqueness, $\varphi$, eight-tick octave, $D=3$) and packages gravity-side consequences once continuum, amplitude, and Page-curve tracks close. Per the module's anti-retreat note and master-plan §6, discovery is not claimed until zero hypothesis inputs remain, the master paper is posted, the §7 falsifier register is populated, and the six §8 done-criteria hold. The PTA and strong-field algebraic witnesses already satisfy the structural half of those tracks; empirical dataset attachments stay separate falsifier obligations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.