gravityS2_residual_lt_one_sigma
plain-language theorem explainer
GRAVITY S2's measured Schwarzschild-precession central value lies inside one sigma of the RS structural target. Strong-field verification and the S2 likelihood certificate cite this residual bound as the compatibility half of the attachment. The proof unfolds the residual, prediction, and sigma constants, then closes by numerical normalization.
Claim. The residual between the GRAVITY S2 central Schwarzschild-precession factor and the RS structural prediction is strictly smaller than the reported one-sigma uncertainty: $\mathrm{residual}_{\mathrm{S2}} < \sigma_{\mathrm{S2}}$. Equivalently, the measured central value is within $1\sigma$ of the RS target $1 + \varphi^{-44}$.
background
This module attaches a dataset-specific likelihood-style certificate to the strong-field falsifier row for the GRAVITY Collaboration (2020) S2 Schwarzschild-precession measurement. Observationally, $f_{\mathrm{SP}} = 1.10 \pm 0.19$, with $f_{\mathrm{SP}} = 0$ Newtonian and $f_{\mathrm{SP}} = 1$ pure GR. The RS structural target is a tiny positive GR deviation written $f_{\mathrm{SP}} = 1 + \varphi^{-44}$.
Sibling constants fix the arithmetic: central value $1.10$, one-sigma width $\sigma$, RS predicted $f_{\mathrm{SP}}$, residual $|\mathrm{central} - \mathrm{RS\ predicted}|$, and target scale $\varphi^{-44}$ (via the phi-power scale map). The shared strong-field dataset attachment records the broader EHT/GRAVITY/Cassini channel and a much smaller RS target scale than current S2 precision.
The local claim is only statistical compatibility at $1\sigma$, not detection of the RS correction.
proof idea
Term-mode numerical check. Unfold the residual, the GRAVITY central value, the RS predicted $f_{\mathrm{SP}}$, the RS target scale, the one-sigma constant, and the strong-field attachment record; then norm_num evaluates the concrete real inequality. No intermediate lemmas are required beyond those definitional equalities.
why it matters
This is fact (1) of the module's two honest claims: GRAVITY's central value is $1\sigma$-compatible with the RS structural target $1 + \varphi^{-44}$. It is wired directly into GravityS2StrongFieldLikelihoodCert as the residual_lt_one_sigma field and into the bundled one-statement theorem that conjoins residual compatibility, non-sensitivity ($\varphi^{-44} \ll 0.19$), and certificate nonemptiness.
In the Recognition verification stack this upgrades the §7 strong-field falsifier row with an S2-specific consistency check. It does not promote the $\varphi^{-44}$ correction to an empirical detection; the companion non-sensitivity theorem records that current GRAVITY precision cannot resolve that scale. Closure status is structural: zero sorry, no new RS-internal axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.