gravityS2StrongFieldLikelihoodCert
plain-language theorem explainer
Packages the five proved GRAVITY S2 likelihood facts into one certificate record: positive σ and RS target scale, residual inside 1σ, target below current precision, and attachment marked not sensitive. Verification authors cite it as the inhabited witness for the S2 strong-field row. Construction is a pure structure instance wiring already-proved positivity and comparison lemmas.
Claim. There is a certificate whose fields assert: the GRAVITY S2 one-sigma uncertainty $\sigma$ is positive; the RS target scale $\phi^{-44}$ is positive; the residual between the GRAVITY central value $f_{SP}=1.10$ and the RS prediction $1+\phi^{-44}$ is strictly less than $\sigma$; the RS target scale is strictly less than $\sigma$ (not currently sensitive); and the strong-field dataset attachment has positive sensitivity, positive target scale, and $currentlySensitive=false$.
background
This module attaches a likelihood-style certificate to the GRAVITY Collaboration (2020) S2 Schwarzschild-precession measurement. Reported data are $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, written structurally as $f_{SP}=1+\phi^{-44}$.
The residual is the absolute gap between the GRAVITY central value and that RS prediction. The one-sigma width is the reported $0.19$. Upstream lemmas already show $\sigma>0$, target scale $>0$, residual $<\sigma$, and target scale $<\sigma$ by unfolding the numeric defs and norm_num. A separate attachment-status theorem records that the strong-field falsifier row is present, positive, and explicitly flagged not currently sensitive.
The certificate structure is the single place those five facts are bundled for downstream Nonempty / one-statement theorems.
proof idea
Pure structure construction. Each field is filled by a named upstream theorem: positivity of $\sigma$ and of the RS target scale; residual strictly inside one sigma; target scale strictly below $\sigma$ (non-sensitivity); and the three-conjunct dataset-attachment status. No new arithmetic is done here; the def only wires those lemmas into the certificate record.
why it matters
Closes the GRAVITY S2 strong-field likelihood attachment as a zero-sorry structural certificate in the Verification domain. Downstream, gravityS2StrongFieldLikelihoodCert_inhabited is the one-line Nonempty witness built from this value, feeding the one-statement S2 likelihood theorem. Module status is structural theorem (closure 2026-05-22): consistency and non-sensitivity only, not empirical confirmation of the $\phi^{-44}$ shift. Sits beside the broader strong-field falsifier register as a second dataset-specific row after the general strong-field structural work.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.