cassiniStrongFieldLikelihoodCert
plain-language theorem explainer
Packages the Cassini Shapiro-delay likelihood certificate: positive one-sigma and RS target scales, residual within 1σ of φ^{-44}, and explicit non-sensitivity of the Bertotti–Iess–Tortora measurement. Gravity and verification workers cite it when attaching the §7 strong-field falsifier row as a Lean certificate rather than a bare dataset flag. Construction is a structure instance that wires five already-proved numeric and attachment lemmas.
Claim. There is a Cassini strong-field likelihood certificate whose fields assert: the reported one-sigma uncertainty $\sigma_\gamma$ on $\gamma-1$ is positive; the RS structural target scale $\varphi^{-44}$ is positive; the residual $|(\gamma-1)_{\mathrm{central}}-\varphi^{-44}|$ is strictly less than $\sigma_\gamma$; $\varphi^{-44}<\sigma_\gamma$ (Cassini is not currently sensitive to the target); and the registered strong-field dataset attachment has positive sensitivity, positive target scale, and $\mathrm{currentlySensitive}=\mathrm{false}$.
background
This module upgrades the §7 strong-field falsifier row from a bare dataset attachment to a dataset-specific likelihood-style Lean certificate. The observational input is the Bertotti–Iess–Tortora Cassini radio-link Shapiro-delay test, $\gamma-1=(2.1\pm 2.3)\times 10^{-5}$. The RS structural target recorded in the falsifier register is $\varphi^{-44}\approx 6.376\times 10^{-10}$.
Sibling constants fix the numerics: cassiniGammaSigma is the reported $2.3\times 10^{-5}$ one-sigma width; cassiniRSTargetScale is the $\varphi^{-44}$ attachment scale; cassiniStrongFieldResidual is the absolute residual between the Cassini central value and that target. The structure CassiniStrongFieldLikelihoodCert bundles five propositions: positivity of $\sigma$ and of the target, residual strictly inside 1$\sigma$, target below $\sigma$ (non-sensitivity), and the register status triple (positive sensitivity, positive target scale, currentlySensitive = false).
Upstream lemmas already discharge each field by norm_num after unfolding, or by the attachment-status conjunction proved from the strong-field register facts. The module states explicitly that this is a consistency / non-sensitivity test, not empirical confirmation.
proof idea
One-line structure instance. Each field is filled by a named upstream lemma: cassiniGammaSigma_pos and cassiniRSTargetScale_pos give the two positivity proofs (unfold + norm_num); cassini_residual_lt_one_sigma shows the residual is below one sigma; cassini_sigma_gt_rs_target shows the target lies below the reported uncertainty (non-sensitivity); cassini_dataset_attachment_status supplies the register triple. No new arithmetic or case analysis occurs at this site.
why it matters
Closes the Cassini half of the §7 strong-field falsifier attachment as a single inhabited certificate. Downstream, cassiniStrongFieldLikelihoodCert_inhabited is the one-line Nonempty witness that quotes this definition, giving a single theorem-shaped handle for the likelihood attachment.
In the Recognition framework this is verification scaffolding around the structural gravity story, not a forcing-chain step (T0–T8). It records that present Cassini precision cannot resolve $\varphi^{-44}$, while the central value remains statistically compatible at 1$\sigma$. That honesty clause (consistency without claiming detection) is what the module status line means by a structural theorem with zero sorry and zero new RS axioms. Parent consumers that need a packaged Cassini certificate rather than five separate lemmas land here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.