rs_strong_field_distinct_GR_prop
plain-language theorem explainer
Names the structural discriminator for RS strong-field gravity: the claim that the RS deviation scale is strictly positive. Anyone citing Track 6.C or the master-theorem witness for strong-field tests uses this proposition. It is a one-line Prop abbreviation of positivity of φ^{-44}, not a proved theorem.
Claim. The structural discriminator proposition asserts $0 < \varphi^{-44}$, i.e. that the RS strong-field deviation signature is strictly positive (hence distinct from pure GR's zero deviation).
background
Track 6.C of the quantum-gravity master plan asks for structural discrimination of RS from pure GR in strong-field channels (S-stars near Sgr A*, EHT shadow, Cassini Shapiro delay, lunar laser ranging). This module ships only the algebraic half: a positive φ-rational signature, not the channel-by-channel post-Newtonian patterns.
The deviation scale is defined as $\varphi^{-44}$, the same rung-44 forcing that yields the baryogenesis ratio $\eta_B = \varphi^{-44}$ on the phi-rung ladder. Pure GR predicts zero structural deviation at this level; RS predicts a strictly positive lower bound at that scale.
Local setting: Gravity Track 6.C structural theorem (zero sorry, zero RS-internal axiom). The master theorem in Gravity.MasterTheorem still needs an inhabitant of the hypothesis that strong-field tests are distinct from GR; this proposition is the Prop that inhabitant will discharge.
proof idea
Definitional, not a proof. The body is the single inequality $0 < \texttt{rs_strong_field_phi_deviation}$, and that quantity is defined upstream as $\varphi^{-44}$. Positivity is proved separately by the companion theorem that $\varphi^{-44} > 0$; this declaration only packages the inequality as a named proposition for the master-theorem interface.
why it matters
This is the Prop half of Track 6.C's structural discriminator. Downstream, rs_strong_field_distinct_GR_prop_holds proves it by invoking positivity of $\varphi^{-44}$; strongFieldDistinctFromGRWitness packages that proof as an inhabitant of StrongFieldTestsDistinctFromGR, retiring the strong-field hypothesis from the conditional quantum-gravity master theorem.
The one-statement theorem and StrongFieldStructuralCert both require this proposition (alongside raw positivity and Nonempty of the master hypothesis). Framework link: rung-44 forcing shared with baryogenesis $\eta_B = \varphi^{-44}$. Open work remains empirical: matching the exact deviation pattern against EHT/GRAVITY/Cassini is a separate falsifier-register obligation, not closed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.