StrongFieldStructuralCert
plain-language theorem explainer
Certificate bundling the structural strong-field discriminator for Track 6.C: the RS deviation scale φ^{-44} is strictly positive, the discriminator proposition holds, and a master-theorem witness that RS strong-field tests differ from pure GR is supplied. Gravity and QG auditors cite it when discharging the StrongFieldTestsDistinctFromGR hypothesis. It is a pure structure definition; the inhabited instance is built elsewhere from positivity and the structural witness.
Claim. A strong-field structural certificate is a triple: (i) $0 < \varphi^{-44}$; (ii) the proposition that the RS strong-field deviation is strictly positive (hence distinct from pure GR's zero baseline); (iii) a witness that RS predictions for strong-field tests (S-stars near Sgr A*, EHT shadow, Cassini Shapiro delay) are distinct from pure GR, as required by the gravity master theorem.
background
Track 6.C of the quantum-gravity master plan asks whether RS strong-field predictions (S-stars near Sgr A*, EHT shadow, lunar laser ranging, Cassini Shapiro delay) differ from pure GR in a checkable way. This module ships only the algebraic discriminator: the RS strong-field deviation signature is $\varphi^{-44}$, the same rung-44 forcing that yields the baryogenesis ratio $\eta_B = \varphi^{-44}$ on the phi-rung ladder.
The deviation is defined as Constants.phi ^ (-44). The structural discriminator proposition is simply $0 < \varphi^{-44}$. Pure GR is treated as the zero-deviation baseline. Upstream, StrongFieldTestsDistinctFromGR is the master-theorem hypothesis interface: a proposition field plus a proof that it holds; the module doc marks the full physics channel work as still open, while the structural positivity is closed.
The certificate packages positivity, the discriminator prop, and an inhabitant of that master hypothesis into one record used by verification and falsifier-sensitivity tracks.
proof idea
No proof body: this is a structure declaration. Its three fields are typed as (1) the inequality $0 < \texttt{rs_strong_field_phi_deviation}$, (2) the proposition rs_strong_field_distinct_GR_prop (definitionally that same positivity), and (3) an inhabitant of Gravity.MasterTheorem.StrongFieldTestsDistinctFromGR. Construction and inhabitation are deferred to strongFieldStructuralCert and strongFieldStructuralCert_inhabited, which fill the fields with rs_strong_field_phi_deviation_pos, rs_strong_field_distinct_GR_prop_holds, and strongFieldDistinctFromGRWitness.
why it matters
Closes the structural half of Track 6.C in the gravity master plan: a theorem-grade, φ-rational signature that pure GR cannot match (zero vs $\varphi^{-44}$). Downstream, strongFieldStructuralCert inhabits the structure, and strongFieldStructuralCert_inhabited records nonemptiness as the one-statement Track 6.C claim. The same certificate is consumed by Track6FalsifierSensitivityCert as one of the theorem-grade discriminator sectors in the Fork F verification lane.
It retires StrongFieldTestsDistinctFromGR from the conditional master theorem's open hypothesis list at the structural level, tying strong-field gravity to the same rung-44 scale as baryogenesis on the phi ladder. Channel-specific observable shifts (precession, shadow diameter, Shapiro delay) remain future physics work; this object only certifies the algebraic distinctness scaffold those derivations must sit on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.