gravityS2_sigma_gt_rs_target
plain-language theorem explainer
GRAVITY's one-sigma uncertainty on the S2 Schwarzschild-precession factor exceeds the Recognition Science structural target scale φ^{-44}. Anyone citing the strong-field non-sensitivity claim for GRAVITY S2 needs this inequality. The proof is a direct numerical comparison after unfolding the two constant definitions.
Claim. The RS structural target scale for the strong-field channel (the numerical stand-in for $\varphi^{-44}$, about $6.376\times 10^{-10}$) is strictly smaller than the GRAVITY Collaboration one-sigma uncertainty $0.19$ on the S2 precession factor $f_{SP}$.
background
The GRAVITY Collaboration (2020) reports the S2 Schwarzschild-precession factor as $f_{SP} = 1.10 \pm 0.19$, with $f_{SP}=0$ Newtonian and $f_{SP}=1$ pure GR. Recognition Science predicts a tiny positive GR deviation of structural form $f_{SP}=1+\varphi^{-44}$.
This module attaches a second dataset-specific likelihood-style certificate to the §7 strong-field falsifier row. The one-sigma width is the constant $0.19$. The RS target scale is taken from the shared strong-field dataset attachment (Cassini / GRAVITY / EHT), whose stored target is $6.376\times 10^{-10}$. The local setting is an honest consistency and non-sensitivity test: zero sorry, zero new RS-internal axioms.
Upstream, the attachment record supplies both the sector label and the numerical target scale used here; sibling positivity facts ensure the compared quantities are positive reals.
proof idea
Unfold the RS target-scale constant, the GRAVITY one-sigma constant $0.19$, and the strong-field attachment record that sources the target. Discharge the resulting concrete real inequality by norm_num. No intermediate lemmas are required beyond definitional unfolding.
why it matters
This inequality is the not_currently_sensitive field of the GRAVITY S2 strong-field likelihood certificate, and the second conjunct of the one-statement attachment theorem that packages residual-within-1σ, non-sensitivity, attachment status, and a nonempty certificate witness.
In the Recognition verification layer it upgrades the §7 strong-field falsifier row for GRAVITY S2: the framework's structural target is a $\varphi^{-44}$ deviation from GR, but current GRAVITY precision ($0.19$) cannot resolve a $10^{-9}$-scale shift. That explicit non-sensitivity is part of the module's structural closure (2026-05-22) and keeps the certificate from overclaiming empirical confirmation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.