cassiniStrongFieldResidual
plain-language theorem explainer
Absolute residual between Cassini’s measured central value of the PPN deviation γ−1 and the Recognition Science strong-field structural target scale. Verification authors cite it when attaching the Bertotti–Iess–Tortora Shapiro-delay result to the §7 falsifier register. The body is a pure definition: the absolute difference of two fixed real constants.
Claim. Define the Cassini strong-field residual by $R := \bigl|(\gamma-1)_{\mathrm{Cassini}} - s_{\mathrm{RS}}\bigr|$, where $(\gamma-1)_{\mathrm{Cassini}} = 2.1\times 10^{-5}$ is the Bertotti–Iess–Tortora central value and $s_{\mathrm{RS}} = \varphi^{-44}$ is the RS structural target scale from the strong-field dataset attachment.
background
The module upgrades the §7 strong-field falsifier row from a bare dataset attachment to a likelihood-style Lean certificate. The dataset is the Cassini radio-link Shapiro-delay test of Bertotti, Iess, and Tortora: $\gamma-1 = (2.1\pm 2.3)\times 10^{-5}$. The RS structural target is $\varphi^{-44}\approx 6.376\times 10^{-10}$, recorded in the strong-field attachment of the falsifier register.
Two sibling constants feed the residual. The Cassini central measurement is the fixed real $2.1\times 10^{-5}$. The RS target scale is the real pulled from strongFieldAttachment.rsTargetScale. The residual is their absolute difference on $\mathbb{R}$.
The certificate’s stated purpose is a consistency / non-sensitivity test, not empirical confirmation: Cassini’s central value sits within $1\sigma$ of the RS scale, yet the target lies far below the reported precision.
proof idea
Pure definition, not a theorem. The body is the absolute value of the difference of the two upstream constants (Cassini central $\gamma-1$ and the RS target scale). No tactics, no lemmas, no unfolding beyond those two defs.
why it matters
This residual is the numeric hinge of the Cassini strong-field likelihood attachment. Downstream, the theorem that the residual is strictly less than the Cassini one-sigma uncertainty unfolds it and discharges the inequality by norm_num. The certificate structure records the same inequality as a field, together with positivity of sigma and target and the flag that the attachment is not currently sensitive. The one-statement theorem packages residual-within-1σ, target-below-sigma, non-sensitivity, and nonemptiness of the certificate.
In the broader Recognition framework this is verification infrastructure for the strong-field falsifier row, not a step of the T0–T8 forcing chain. It makes precise that Cassini is compatible with, but presently insensitive to, the RS scale $\varphi^{-44}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.