cassiniGammaSigma
plain-language theorem explainer
Defines the Cassini one-sigma uncertainty on the PPN parameter γ−1 as 2.3×10⁻⁵, taken from the Bertotti–Iess–Tortora radio-link Shapiro-delay measurement. Anyone building the Cassini strong-field likelihood certificate cites this constant as the experimental error bar. It is a bare real literal, not a derived quantity.
Claim. The Cassini one-sigma uncertainty on $\gamma - 1$ is the real constant $\sigma_\gamma := 2.3 \times 10^{-5}$.
background
The module attaches the Cassini radio-link Shapiro-delay test to the Recognition Science strong-field falsifier row. The published measurement is $\gamma - 1 = (2.1 \pm 2.3)\times 10^{-5}$. The RS structural target for the same residual is $\varphi^{-44}\approx 6.376\times 10^{-10}$, recorded in the §7 dataset attachment strongFieldAttachment.
In the PPN formalism, $\gamma$ measures how much space curvature is produced by unit rest mass; GR predicts $\gamma=1$ exactly. Cassini constrains the deviation $\gamma-1$ at the few-parts-in-$10^5$ level. The present definition freezes that reported one-sigma half-width as a Lean real so later residual and sensitivity comparisons can be discharged by norm_num.
The certificate is deliberately a consistency / non-sensitivity test: it does not claim empirical confirmation of the RS target, only that the central value sits inside 1σ of the target and that the target lies far below current precision.
proof idea
Pure definitional assignment: the real literal 2.3e-5 is bound to the name. No lemmas, no tactics. Downstream positivity and comparison theorems simply unfold this constant and finish with norm_num.
why it matters
This constant is the experimental error bar that every Cassini likelihood fact in the module compares against. It feeds cassiniGammaSigma_pos (positivity), cassini_residual_lt_one_sigma (central value within 1σ of the RS target), and cassini_sigma_gt_rs_target (target scale below the reported precision). Those three facts are packaged into the structure CassiniStrongFieldLikelihoodCert and the one-statement theorem cassini_strong_field_likelihood_one_statement.
In the broader RS verification stack this closes the §7 strong-field falsifier row as a dataset-specific likelihood-style certificate: zero sorry, zero new RS axioms. The scientific content is honest non-sensitivity: $\varphi^{-44}$ is many orders of magnitude below $2.3\times 10^{-5}$, so Cassini cannot yet probe the RS strong-field scale. The definition therefore anchors a negative but necessary claim in the falsifier register.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.