gravityS2FSPSigma
plain-language theorem explainer
The GRAVITY Collaboration S2 one-sigma uncertainty on the Schwarzschild-precession factor f_SP is fixed at the reported value 0.19. Verification authors cite this constant when proving residual compatibility with the RS structural target and when showing that GRAVITY is not yet sensitive to φ^{-44}. The body is a bare real literal, not a derived quantity.
Claim. The one-sigma uncertainty on the GRAVITY S2 Schwarzschild-precession factor is $\sigma_{f_{SP}} = 0.19$, matching the published GRAVITY Collaboration (2020) error bar on $f_{SP} = 1.10 \pm 0.19$.
background
This module attaches a likelihood-style certificate to the GRAVITY Collaboration (2020) S2 Schwarzschild-precession measurement. The reported parameter is $f_{SP} = 1.10 \pm 0.19$, where $f_{SP} = 0$ is Newtonian and $f_{SP} = 1$ is general relativity.
Recognition Science predicts a tiny positive deviation from GR, written structurally as $f_{SP} = 1 + \varphi^{-44}$. The certificate checks two honest facts: the GRAVITY central value sits within $1\sigma$ of that RS target, and the RS target scale itself lies far below the reported $0.19$ precision, so the dataset is not currently sensitive.
Sibling constants in the same file fix the GRAVITY central value, the RS target scale $\varphi^{-44}$, and the residual between them. This definition supplies only the experimental error bar used in those comparisons.
proof idea
No proof. The declaration is a one-line real constant equal to the published GRAVITY $1\sigma$ uncertainty $0.19$. Downstream positivity and comparison theorems simply unfold this name and discharge the resulting numeric goals with norm_num.
why it matters
The constant is the experimental half of the GRAVITY S2 strong-field attachment. It is required by gravityS2FSPSigma_pos (positivity), by gravityS2_residual_lt_one_sigma (central value within $1\sigma$ of the RS target), and by gravityS2_sigma_gt_rs_target (uncertainty larger than $\varphi^{-44}$, hence non-sensitivity).
Those three facts pack into the certificate structure GravityS2StrongFieldLikelihoodCert and the one-statement theorem gravity_s2_strong_field_likelihood_one_statement. Together they close the §7 strong-field falsifier row for S2 as a consistency and non-sensitivity test, not as empirical confirmation of the RS mass or curvature ladder. The module status is structural theorem: zero sorry, zero new RS-internal axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.