GravityS2StrongFieldLikelihoodCert
plain-language theorem explainer
Packages the GRAVITY S2 strong-field likelihood certificate: positive experimental σ and RS target scale, residual of the S2 precession factor below 1σ, RS target below reported precision (not currently sensitive), and the strong-field dataset row marked positive yet insensitive. Aggregate falsifier-likelihood registers and the one-statement S2 theorem cite it. Pure structure of already-proved inequalities; no proof body.
Claim. A certificate record asserting five facts about the GRAVITY S2 precession factor $f_{SP}$: (i) the reported one-sigma uncertainty $\sigma$ is positive; (ii) the RS structural target scale $\delta_{\mathrm{RS}}$ is positive; (iii) the residual $|f_{SP}^{\mathrm{obs}}-f_{SP}^{\mathrm{RS}}|<\sigma$; (iv) $\delta_{\mathrm{RS}}<\sigma$ (experiment not currently sensitive to the RS deviation); (v) the strong-field dataset attachment has positive sensitivity and positive RS target scale, and is flagged as not currently sensitive.
background
This module attaches a dataset-specific likelihood-style certificate to the GRAVITY Collaboration (2020) S2 Schwarzschild-precession measurement. The reported value is $f_{SP}=1.10\pm 0.19$, with $f_{SP}=0$ Newtonian and $f_{SP}=1$ pure GR. Recognition Science predicts a tiny positive deviation from GR, written structurally as $f_{SP}=1+\varphi^{-44}$.
The one-sigma width is the constant $0.19$. The residual is the absolute gap between GRAVITY's central value and the RS-predicted $f_{SP}$. The RS target scale is taken from the shared strong-field dataset attachment (Cassini / GRAVITY / EHT row), whose sensitivity and rsTargetScale are required to be positive by the falsifier-register predicates.
The local setting is a consistency and non-sensitivity test, not empirical confirmation: the certificate records that the RS target sits well inside the error bar and far below current precision.
proof idea
No proof body: this is a structure definition. Its five fields are Prop-valued obligations (positivity of $\sigma$ and of the RS target scale, residual strictly below one sigma, target scale strictly below $\sigma$, and the three-way dataset-status conjunction). Inhabitation is supplied downstream by a concrete constructor that fills each field with the corresponding named lemma (gravityS2FSPSigma_pos, gravityS2RSTargetScale_pos, residual and sensitivity inequalities, and the dataset-attachment status theorem).
why it matters
Closes the GRAVITY S2 half of the §7 strong-field falsifier upgrade. Downstream, the inhabited instance and the one-statement theorem package residual-below-sigma, target-below-sigma, and currentlySensitive = false into a single Nonempty certificate. That certificate is a required field of the aggregate FalsifierLikelihoodRegisterCert alongside the Planck $\Omega_\Lambda$ and Cassini strong-field likelihood certs.
In the Recognition framework this is an honest non-sensitivity ledger entry: the structural RS deviation $\varphi^{-44}$ is compatible with GRAVITY at 1σ yet remains invisible to present precision. It does not advance the T0–T8 forcing chain; it records that the strong-field channel has not yet reached the RS target scale. Status is structural (zero sorry, zero new RS axioms).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.