gravity_s2_strong_field_likelihood_one_statement
plain-language theorem explainer
GRAVITY's S2 Schwarzschild-precession factor is within 1σ of the RS structural target, yet the experiment is not currently sensitive to the RS deviation scale φ^{-44}. Auditors of the §7 strong-field falsifier row cite this as the single packaged likelihood-attachment statement. The proof is a four-component term assembling two numerical inequalities, reflexivity on the attachment flag, and certificate inhabitance.
Claim. The residual between GRAVITY's central $f_{SP}$ and the RS structural prediction is strictly less than the reported one-sigma $0.19$; the RS target deviation scale is also strictly less than $0.19$; the strong-field dataset attachment is marked not currently sensitive; and the GRAVITY S2 strong-field likelihood certificate is inhabited.
background
This module upgrades the §7 strong-field falsifier row with a dataset-specific likelihood-style certificate for the GRAVITY Collaboration (2020) S2 Schwarzschild-precession measurement. GRAVITY reports $f_{SP} = 1.10 \pm 0.19$, where $f_{SP}=0$ is Newtonian and $f_{SP}=1$ is GR. Recognition Science predicts a tiny positive deviation from GR, written structurally as $f_{SP} = 1 + \varphi^{-44}$.
The residual is the absolute difference between GRAVITY's central value and the RS-predicted FSP. The one-sigma uncertainty is the constant $0.19$. The RS target scale is read from the strong-field dataset attachment (Cassini Shapiro delay; GRAVITY S2; EHT M87* shadow), whose stored rsTargetScale is about $6.4\times 10^{-10}$. Upstream lemmas already establish residual $<$ sigma and target scale $<$ sigma by unfolding and norm_num.
The certificate structure packages positivity of sigma and target, the two inequalities, and the attachment status (positive sensitivity, positive target scale, and currentlySensitive = false).
proof idea
Pure term proof: a four-tuple. The first two conjuncts are the named lemmas that residual $<$ one-sigma and RS target scale $<$ one-sigma (each proved by unfolding the numeric defs and norm_num). The third conjunct is reflexivity on the attachment flag currentlySensitive = false. The fourth is inhabitance of the certificate structure, which itself packages the same inequalities plus positivity and dataset-status facts.
why it matters
Closes the GRAVITY S2 strong-field likelihood attachment as a structural theorem (0 sorry, 0 new RS axioms; module status closed 2026-05-22). It upgrades the §7 strong-field falsifier row with an honest consistency / non-sensitivity test: GRAVITY's central value sits inside 1σ of the RS target, but $\varphi^{-44}$ lies far below the reported $0.19$ precision, so the dataset cannot yet discriminate. No downstream consumers are wired yet. The statement is deliberately not empirical confirmation of RS over GR; it only certifies that the present error bar does not falsify the structural target and does not resolve it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.