gravityS2FSPCentral
plain-language theorem explainer
Fixes the GRAVITY Collaboration (2020) S2 central value of the Schwarzschild-precession factor at 1.10 (where 0 is Newtonian and 1 is GR). Downstream residual and 1σ-compatibility certificates cite this constant as the observational anchor. The body is a bare real literal; no proof work.
Claim. The GRAVITY S2 central measurement of the Schwarzschild-precession factor is $f_{\mathrm{SP}}^{\mathrm{obs}} = 1.10$.
background
The module attaches a likelihood-style certificate to the GRAVITY Collaboration (2020) S2 stellar-orbit precession around Sgr A*. The reported datum 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 tiny positive structural deviation from GR, written $f_{\mathrm{SP}} = 1 + \varphi^{-44}$. The certificate only checks two honest facts: the observed central value sits inside 1σ of that target, and the RS scale $\varphi^{-44}$ lies far below the reported 0.19 precision (non-sensitivity).
This constant is the observational centre used by the residual $|\mathrm{central} - \mathrm{RS\ target}|$ and by the inequality that residual is strictly less than the one-sigma width.
proof idea
Definitional constant: the real literal 1.10 is assigned directly. No tactics, lemmas, or algebraic reduction.
why it matters
Anchors the GRAVITY S2 strong-field falsifier row in the verification layer. The residual definition subtracts the RS structural prediction from this centre; the theorem gravityS2_residual_lt_one_sigma then unfolds both and discharges the 1σ bound by norm_num.
Together with the companion sigma and RS-target-scale constants, it closes a consistency / non-sensitivity test (module status: structural theorem, 0 sorry, 0 new RS axioms). It does not claim empirical confirmation of $\varphi^{-44}$; it only records that current GRAVITY precision cannot see that scale. Feeds the broader strong-field attachment certificate for the §7 falsifier register.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.