cassiniStrongFieldLikelihoodCert_inhabited
plain-language theorem explainer
The Cassini strong-field likelihood certificate type is inhabited: a concrete witness packages positivity of the reported one-sigma and of the RS target scale φ^{-44}, residual-within-1σ compatibility, and explicit non-sensitivity. Verification authors cite it when assembling the falsifier likelihood register. The proof is a one-line term that exhibits the prebuilt certificate value.
Claim. The type of Cassini strong-field likelihood certificates is nonempty: there exists a record asserting $0 < \sigma_{\gamma}$, $0 < \phi^{-44}$, residual $|(\gamma-1)_{\mathrm{obs}} - \phi^{-44}| < \sigma_{\gamma}$, $\phi^{-44} < \sigma_{\gamma}$, and that 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 test, $\gamma - 1 = (2.1 \pm 2.3)\times 10^{-5}$. The RS structural target is $\phi^{-44} \approx 6.376\times 10^{-10}$, recorded in the strong-field attachment of the falsifier register.
The certificate structure bundles five honest facts: positivity of Cassini's reported one-sigma and of the RS target scale; that the residual of the central value against the RS target lies inside one sigma; that the target lies far below the experimental precision (not currently sensitive); and that the shared dataset attachment flags positive sensitivity, positive target, and currentlySensitive = false.
This is a consistency / non-sensitivity test, not empirical confirmation of the RS prediction. The module claims zero sorry and zero new RS-specific axioms.
proof idea
One-line term proof. The inhabitant is the already-constructed value cassiniStrongFieldLikelihoodCert, which fills every field of the certificate structure from the sibling lemmas: positivity of $\sigma_\gamma$ and of the RS target, residual strictly below one sigma, target strictly below $\sigma_\gamma$, and the dataset-attachment status triple. Nonemptiness is then just the anonymous constructor around that value.
why it matters
Feeds the one-statement Cassini likelihood attachment theorem, which conjoins residual-within-1σ, non-sensitivity, the attachment flag, and this Nonempty fact into a single export. Also plugs directly into the falsifier likelihood register certificate as the Cassini slot, alongside Ω_Λ, Gravity S2, EHT M87, and NANOGrav PTA inhabited certificates.
In the Recognition framework this closes the strong-field Cassini row of the verification layer: GR-compatible Cassini data do not rule out the tiny RS structural correction $\phi^{-44}$, and the formal certificate records that the experiment is presently insensitive to that scale. It is structural bookkeeping for the falsifier register, not a mass or coupling derivation from the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.