CassiniStrongFieldLikelihoodCert
plain-language theorem explainer
Bundles the Cassini Shapiro-delay likelihood certificate: positive one-sigma on γ−1, positive RS target scale, residual under 1σ, target below experimental precision, and dataset attachment marked not currently sensitive. Downstream inhabited and one-statement theorems, plus the aggregate falsifier likelihood register, cite this bundle. Pure structure definition; fields are discharged by sibling positivity and comparison lemmas.
Claim. A certificate packing five facts about the Cassini radio-link Shapiro-delay test of $\gamma-1$: the reported one-sigma $\sigma$ is positive; the RS strong-field target scale $t$ is positive; the residual $|(\gamma-1)_{\mathrm{cent}}-t|$ is strictly less than $\sigma$; $t<\sigma$ (experiment not currently sensitive to the RS scale); and the 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 dataset is the Bertotti–Iess–Tortora Cassini radio-link Shapiro-delay measurement $\gamma-1=(2.1\pm 2.3)\times 10^{-5}$. The RS structural target is $\varphi^{-44}\approx 6.376\times 10^{-10}$, stored on the strong-field attachment (sector: strong-field / precision-GR tests; also lists GRAVITY S2 and EHT M87*).
Sibling defs fix the numbers: one-sigma uncertainty $\sigma=2.3\times 10^{-5}$; RS target scale pulled from the attachment; residual as absolute deviation of the Cassini central value from that target. Upstream predicates HasPositiveSensitivity and HasPositiveTargetScale simply require $0<$ sensitivity and $0<$ rsTargetScale on a DatasetAttachment.
The module status is structural theorem: zero sorry, zero new RS-internal axioms. The intended reading is consistency / non-sensitivity, not empirical confirmation of the RS scale.
proof idea
No proof body: this is a structure whose five fields are propositions. Inhabitation is supplied downstream by a concrete value that fills each field from named sibling lemmas: positivity of $\sigma$ and of the RS target, residual strictly below one sigma, target strictly below $\sigma$, and the three-way dataset-status conjunction (positive sensitivity, positive target, currentlySensitive = false by reflexivity on the attachment record).
why it matters
Closes the Cassini half of the strong-field likelihood attachment in the verification layer. The concrete certificate value, the Nonempty inhabitation theorem, and the one-statement conjunction (residual $<\sigma$, target $<\sigma$, not currently sensitive, and nonempty cert) all depend on this structure. Upstream of the aggregate FalsifierLikelihoodRegisterCert, which requires a nonempty Cassini strong-field likelihood cert alongside OmegaLambda/Planck and GRAVITY S2 rows.
In the Recognition framework this is honest bookkeeping on the PPN-$\gamma$ channel: the RS target $\varphi^{-44}$ sits far below Cassini precision, so the row is marked not currently sensitive while still recording 1$\sigma$ compatibility of the central value. It does not invoke the forcing chain (T0–T8) or the RCL directly; it is a verification-side attachment that keeps the falsifier register from overclaiming empirical reach.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.