cassini_strong_field_likelihood_one_statement
plain-language theorem explainer
Packages the Cassini Shapiro-delay check into one conjunction: the residual of γ−1 from the RS target is below 1σ, the φ⁻⁴⁴ target sits below Cassini’s reported σ, the dataset is flagged not currently sensitive, and a likelihood certificate exists. Verification authors cite it as the single export of the Cassini strong-field row. The proof is a four-component term pairing two norm_num lemmas, rfl, and certificate inhabitation.
Claim. The absolute residual between Cassini’s central $\gamma-1=(2.1\pm 2.3)\times 10^{-5}$ and the RS structural target scale is strictly less than the reported one-sigma uncertainty $2.3\times 10^{-5}$; that same uncertainty strictly exceeds the RS target; the strong-field falsifier attachment is marked not currently sensitive; and a Cassini strong-field likelihood certificate is inhabited.
background
The module upgrades the §7 strong-field falsifier row from a bare dataset attachment to a dataset-specific likelihood-style Lean certificate. The dataset is the Bertotti–Iess–Tortora Cassini radio-link Shapiro-delay test, with $\gamma-1=(2.1\pm 2.3)\times 10^{-5}$. The RS structural target is $\varphi^{-44}\approx 6.376\times 10^{-10}$, taken from strongFieldAttachment in the falsifier register.
Local constants fix the reported one-sigma width at $2.3\times 10^{-5}$ and the residual as the absolute gap between Cassini’s central value and the RS target scale. Upstream lemmas already show the residual is below 1σ and that Cassini’s σ exceeds the target (so the experiment is not currently sensitive to $\varphi^{-44}$). The certificate structure bundles positivity of σ and target, those two inequalities, and the attachment’s positive-sensitivity / positive-target / not-sensitive status flags.
This is framed as a consistency and non-sensitivity test, not empirical confirmation of the RS prediction.
proof idea
Term-mode four-tuple. First component is cassini_residual_lt_one_sigma (unfold residual, central value, target, σ, and attachment, then norm_num). Second is cassini_sigma_gt_rs_target (same unfold-and-norm_num pattern for target $<$ σ). Third is rfl on strongFieldAttachment.currentlySensitive = false. Fourth is cassiniStrongFieldLikelihoodCert_inhabited, which witnesses Nonempty of the certificate structure via the concrete inhabitant already assembled in-module.
why it matters
Closes the Cassini strong-field likelihood attachment as a single proved export: residual compatibility at 1σ, honest non-sensitivity of Cassini to $\varphi^{-44}$, and an inhabited certificate structure. Module status is structural theorem (0 sorry, 0 new RS-internal axioms; closure 2026-05-22). It upgrades the §7 falsifier-register row from dataset attachment to a likelihood-style certificate without claiming empirical confirmation.
No downstream dependents are recorded yet; the declaration is the module’s public one-statement summary. In the broader Recognition framework it sits in Verification rather than the T0–T8 forcing chain: it checks that a published PPN-γ bound is consistent with, and currently too coarse to probe, the RS strong-field structural scale. The open scientific question it leaves explicit is future sensitivity: only a much tighter σ could turn the non-sensitivity flag into a genuine test of $\varphi^{-44}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.