gravityS2FSPSigma_pos
plain-language theorem explainer
The GRAVITY S2 one-sigma uncertainty on the Schwarzschild precession factor is strictly positive. Anyone assembling the strong-field likelihood certificate cites this positivity side-condition. The proof unfolds the numeric definition 0.19 and discharges the inequality by norm_num.
Claim. Let $\sigma_{\mathrm{S2}}$ be the reported one-sigma uncertainty on the GRAVITY Collaboration S2 Schwarzschild-precession factor $f_{\mathrm{SP}}$. Then $0 < \sigma_{\mathrm{S2}}$, where $\sigma_{\mathrm{S2}} = 0.19$.
background
The module attaches a dataset-specific likelihood-style certificate to the §7 strong-field falsifier row, using the GRAVITY Collaboration (2020) S2 precession measurement $f_{\mathrm{SP}} = 1.10 \pm 0.19$. Here $f_{\mathrm{SP}} = 0$ is Newtonian and $f_{\mathrm{SP}} = 1$ is GR. The RS structural target is a tiny positive deviation $f_{\mathrm{SP}} = 1 + \varphi^{-44}$.
The one-sigma width $\sigma_{\mathrm{S2}} := 0.19$ is the reported experimental uncertainty on $f_{\mathrm{SP}}$. Downstream residual and sensitivity comparisons treat this width as a positive real scale, so the certificate structure requires an explicit positivity lemma before those inequalities can be stated.
proof idea
One-line numeric discharge: unfold the definition of the S2 one-sigma constant to the literal $0.19$, then apply norm_num to obtain $0 < 0.19$. No external lemmas are needed.
why it matters
This lemma fills the sigma_pos field of GravityS2StrongFieldLikelihoodCert, the structural certificate that packages two honest facts: (1) GRAVITY's central value is compatible with the RS target at $1\sigma$, and (2) GRAVITY is not currently sensitive to the RS scale $\varphi^{-44}$, which lies far below the $0.19$ precision. Without positivity of $\sigma$, residual-to-sigma ratios and the non-sensitivity comparison $\sigma > \varphi^{-44}$ are ill-typed as strict inequalities over $\mathbb{R}$. The module is a consistency / non-sensitivity test, not empirical confirmation of the RS strong-field prediction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.