cassiniRSTargetScale_pos
plain-language theorem explainer
The RS structural target scale for the Cassini Shapiro-delay row is strictly positive. Anyone assembling the Cassini strong-field likelihood certificate needs this positivity field. The proof unfolds the target to the recorded strong-field attachment constant and finishes by numeric normalization.
Claim. The Recognition Science structural target scale attached to the Cassini radio-link Shapiro-delay test is strictly positive: $0 < \varphi^{-44}$ (the value recorded as the strong-field attachment scale).
background
This module upgrades the §7 strong-field falsifier row into a dataset-specific likelihood-style Lean certificate for the Bertotti–Iess–Tortora Cassini radio-link Shapiro-delay measurement $\gamma-1=(2.1\pm 2.3)\times 10^{-5}$.
The RS structural target on that row is $\varphi^{-44}\approx 6.376\times 10^{-10}$, stored as the strong-field attachment scale in the falsifier-register datasets. Phi-powers appear throughout RS as the native ladder of scales (the cosmology helper scale k := phi^k is the same family). The certificate is deliberately a consistency / non-sensitivity check, not empirical confirmation: Cassini’s one-sigma width sits far above the target.
Positivity of that target scale is a trivial but required field of the certificate structure, so downstream packing does not smuggle a non-positive scale into residual and sensitivity comparisons.
proof idea
One short tactic proof. Unfold the local target-scale definition together with the strong-field attachment constant it aliases, then run norm_num on the resulting concrete positive real. No lemmas beyond definitional reduction and numeric positivity are required.
why it matters
Feeds the target_pos field of cassiniStrongFieldLikelihoodCert, the inhabited certificate that packages four honest facts: sigma positivity, target positivity, residual within 1σ of the RS scale, and current non-sensitivity (Cassini sigma larger than the RS target). Without this lemma the certificate structure cannot be filled.
In the broader RS verification layer this closes a structural obligation on the strong-field falsifier row: the recorded $\varphi^{-44}$ target is a legitimate positive scale before any residual or sensitivity comparison is stated. It does not touch the forcing chain (T0–T8) or the Recognition Composition Law; it is pure verification hygiene on an already-chosen ladder rung.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.