cassini_dataset_attachment_status
plain-language theorem explainer
The Cassini strong-field dataset attachment has positive sensitivity, a positive RS target scale, and is explicitly flagged as not currently sensitive. Verification authors cite it when assembling the Cassini likelihood certificate. The proof is a three-component term pairing two positivity lemmas with reflexivity on the sensitivity flag.
Claim. For the strong-field dataset attachment (Cassini Shapiro delay / GRAVITY / EHT row), the recorded sensitivity is positive, the RS target scale is positive, and the attachment's currently-sensitive flag equals false.
background
This module turns the §7 strong-field falsifier row into a dataset-specific likelihood-style certificate for the Bertotti–Iess–Tortora Cassini radio-link Shapiro-delay test, $\gamma-1=(2.1\pm 2.3)\times 10^{-5}$. The RS structural target stored on the attachment is $\varphi^{-44}\approx 6.376\times 10^{-10}$.
A DatasetAttachment records sector, dataset string, units, numerical sensitivity, and RS target scale. Positive sensitivity means $0<$ sensitivity; positive target scale means $0<$ rsTargetScale. The strong-field attachment sets sensitivity to $2.3\times 10^{-5}$ (Cassini one-sigma precision) and rsTargetScale to $6.376\times 10^{-10}$.
Upstream lemmas already prove those two inequalities by unfolding the attachment record and norm_num. The module stresses this is a consistency / non-sensitivity test, not empirical confirmation of RS.
proof idea
Term-mode proof of a three-way conjunction. The first conjunct is discharged by strongField_sensitivity_pos (unfolds HasPositiveSensitivity on the strong-field attachment and closes by norm_num). The second is strongField_target_pos by the same pattern on HasPositiveTargetScale. The third is rfl on the boolean field currentlySensitive = false as defined on the attachment record.
why it matters
Feeds the master certificate cassiniStrongFieldLikelihoodCert as the dataset_status field of CassiniStrongFieldLikelihoodCert. That cert packages four honest facts: positive Cassini $\sigma$, positive RS target, residual below one sigma, and $\sigma$ larger than the RS target (not currently sensitive), plus this attachment-status triple.
In the Recognition verification stack this closes the strong-field row of the falsifier register for Cassini: the attachment is present and numerically well-formed, yet the experiment cannot yet resolve $\varphi^{-44}$. It supports the module claim of structural theorem status (zero sorry, zero new RS axioms) without overclaiming detection. Downstream consumers of the likelihood cert inherit a machine-checked non-sensitivity statement rather than an informal note.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.