strongFieldDistinctFromGRWitness
plain-language theorem explainer
Packages the structural claim that the RS strong-field deviation equals $\varphi^{-44}$ and is strictly positive, while pure GR predicts zero. Partial quantum-gravity master theorems cite this witness to discharge Track 6.C. It is a structure inhabitant wiring the discriminator proposition to its positivity proof.
Claim. There is an inhabitant of the Track 6.C hypothesis structure "RS strong-field tests are distinct from pure GR": its proposition is $0 < \varphi^{-44}$ (the RS strong-field deviation signature), and that inequality holds.
background
Track 6.C of the quantum-gravity master plan asks for RS predictions on strong-field probes (S-stars near Sgr A*, EHT shadow, Cassini Shapiro delay, lunar laser ranging) that differ from pure GR. This module supplies only the algebraic discriminator: the RS deviation is the positive $\varphi$-rational $\varphi^{-44}$, the same rung-44 forcing scale that yields $\eta_B = \varphi^{-44}$ on the phi-rung ladder, while pure GR has zero deviation.
The master-theorem input structure (from Gravity.MasterTheorem) carries a proposition field together with a proof that it holds. Locally that proposition is defined as $0 < \varphi^{-44}$, and the positivity theorem for $\varphi^{-44}$ discharges it. Specific per-channel deviation patterns remain out of scope here.
proof idea
Structure inhabitant, not a tactic proof. The proposition field is set to the local discriminator $0 < \varphi^{-44}$; the holds field is filled by the already-proved positivity lemma for that quantity (itself a one-line appeal to positivity of a negative power of $\varphi > 1$). No new algebra is performed at this site.
why it matters
Retires the strong-field hypothesis from the conditional RS quantum-gravity master theorem: partial and deeper-partial master statements thread this witness as a concrete argument, so Track 6.C no longer appears as an open hypothesis on those paths. Downstream users include the partial conditional master theorem and its $\forall$-quantified form, plus the structural master-theorem certificate and honest-scope statement.
Framework link: the deviation scale is the same $\varphi^{-44}$ rung that forces the baryon asymmetry scale on the phi-ladder. The module is marked structural closure (0 sorry); observational channel physics is explicitly deferred.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.