gravityS2Residual
plain-language theorem explainer
Absolute residual between the GRAVITY Collaboration S2 central Schwarzschild-precession factor and the Recognition Science structural target. Verification authors cite it when checking 1σ compatibility of the S2 row. It is a one-line absolute-difference definition of two named constants.
Claim. Define the residual $R := |f_{\mathrm{SP}}^{\mathrm{obs}} - f_{\mathrm{SP}}^{\mathrm{RS}}|$, where $f_{\mathrm{SP}}^{\mathrm{obs}} = 1.10$ is the GRAVITY S2 central value and $f_{\mathrm{SP}}^{\mathrm{RS}} = 1 + \varphi^{-44}$ is the RS structural target (GR plus a tiny positive shift).
background
This module attaches a likelihood-style certificate to the GRAVITY Collaboration (2020) S2 Schwarzschild-precession measurement. The reported factor is $f_{\mathrm{SP}} = 1.10 \pm 0.19$, with $f_{\mathrm{SP}} = 0$ Newtonian and $f_{\mathrm{SP}} = 1$ pure GR.
Recognition Science predicts a minute positive deviation from GR, written structurally as $f_{\mathrm{SP}} = 1 + \varphi^{-44}$. The central GRAVITY value is fixed as the constant $1.10$; the RS prediction is $1$ plus the target scale $\varphi^{-44}$.
The residual is the absolute gap between those two numbers. Downstream theorems compare it to the reported one-sigma width $0.19$ to establish statistical compatibility and non-sensitivity.
proof idea
Pure definition: unfold to the absolute value of the difference between the GRAVITY central constant and the RS predicted factor. No lemmas, no tactics; the body is literally $|\mathrm{central} - \mathrm{RS\ predicted}|$.
why it matters
Feeds the 1σ compatibility theorem (residual strictly less than the GRAVITY sigma), the certificate structure that packages positivity and non-sensitivity, and the one-statement likelihood attachment theorem. Together those close the §7 strong-field falsifier row for S2 as a consistency / non-sensitivity test: the data sit inside 1σ of the RS target, yet $\varphi^{-44}$ lies far below current precision, so GRAVITY cannot yet resolve the RS shift. Zero sorry, zero new RS axioms; structural closure only.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.