gravityS2RSPredictedFSP
plain-language theorem explainer
The RS structural prediction for the GRAVITY S2 Schwarzschild precession factor is the GR baseline plus a φ^{-44} correction. Verification authors cite this constant when attaching the S2 likelihood certificate and forming the residual against GRAVITY's central value. It is a one-line definition that adds the structural target scale to the GR value 1.
Claim. The Recognition Science predicted S2 precession factor is $f_{\mathrm{SP}}^{\mathrm{RS}} = 1 + s$, where $1$ is the GR value of the Schwarzschild precession factor and $s = \varphi^{-44}$ is the RS structural target scale.
background
The module attaches a dataset-specific likelihood-style certificate to the GRAVITY Collaboration (2020) S2 Schwarzschild-precession measurement. Reported data are $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 tiny positive deviation from GR, written structurally as $f_{\mathrm{SP}} = 1 + \varphi^{-44}$. The sibling constant gravityS2RSTargetScale is that $\varphi^{-44}$ scale; this definition simply places it on top of the GR baseline.
The setting is a consistency / non-sensitivity test for the §7 strong-field falsifier row: check that GRAVITY's central value sits within 1σ of the RS target, and that the target scale itself lies far below the reported 0.19 precision.
proof idea
Pure definitional assembly: the real is defined as one plus the RS target scale constant. No tactics, no lemmas, no analytic evaluation. Downstream residual and inequality proofs unfold this name together with the central value, sigma, and target-scale definitions, then discharge the numeric comparison by norm_num.
why it matters
This constant is the RS side of the S2 residual. The residual definition takes the absolute difference between GRAVITY's central value and this predicted factor; the theorem gravityS2_residual_lt_one_sigma then proves that residual is strictly less than the reported one-sigma width.
Together those facts close the structural certificate: GRAVITY is statistically compatible with $1 + \varphi^{-44}$ at 1σ, yet not currently sensitive to a correction of size $\varphi^{-44}$. The module status is a structural theorem with zero sorry and zero new RS-internal axioms (closure 2026-05-22). It upgrades the strong-field falsifier row without claiming empirical confirmation of the RS deviation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.