strongFieldStructuralCert
plain-language theorem explainer
Packages three already-proved facts into one certificate: the RS strong-field deviation φ^{-44} is strictly positive, the structural discriminator against pure GR holds, and the master-theorem hypothesis that strong-field tests distinguish RS from GR is inhabited. Gravity-track auditors cite it as the Track 6.C structural closure object. The body is a three-field structure instance wiring existing positivity and witness lemmas.
Claim. There is a certificate packing (i) $0 < \varphi^{-44}$, (ii) the structural claim that the RS strong-field deviation is strictly positive while pure GR predicts zero deviation, and (iii) an inhabitant of the master-theorem hypothesis that strong-field tests distinguish RS from pure GR.
background
Track 6.C of the quantum-gravity master plan asks for structural discriminators on strong-field tests (S-stars near Sgr A*, EHT shadow, lunar laser ranging, Cassini Shapiro delay). This module supplies the algebraic form only: RS carries a positive φ-rational deviation signature, pure GR carries zero.
The deviation is identified with $\varphi^{-44}$, the same rung-44 forcing scale that yields $\eta_B = \varphi^{-44}$ on the cosmology φ-ladder. Positivity $0 < \varphi^{-44}$ follows from $\varphi > 0$ and the usual positive-power law for integer powers. The discriminator proposition is exactly that strict positivity against GR's zero baseline.
The master theorem in Gravity.MasterTheorem takes a hypothesis input asserting that strong-field tests distinguish RS from GR. The local witness inhabits that input and thereby retires the hypothesis from the conditional master theorem.
proof idea
One-line structure construction. Field deviation_pos is filled by the positivity theorem for $\varphi^{-44}$ (unfold the deviation definition, apply zpow_pos with $\varphi > 0$). Field discriminator_holds is the one-line reduction of the discriminator proposition to that same positivity fact. Field master_hypothesis_witness is the existing inhabitant of the master-theorem hypothesis record, whose two fields are the discriminator proposition and its proof.
why it matters
This is the §4 master cert of Track 6.C in structural form. Downstream, strongFieldStructuralCert_inhabited records Nonempty of the certificate type by wrapping this value, giving the one-statement Track 6.C closure: the RS deviation $\varphi^{-44}$ is strictly positive and distinct from pure GR's zero.
More importantly, the packed master-hypothesis witness retires StrongFieldTestsDistinctFromGR from the conditional quantum-gravity master theorem, converting a named hypothesis into a discharged input. The module status line marks full structural closure (0 sorry, 0 RS-internal axiom). Channel-specific observable shifts (S-stars, EHT, LLR, Cassini) are separate strengthenings; this cert is the bare structural spine those channels refine.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.