cassiniRSTargetScale
plain-language theorem explainer
Names the RS strong-field structural target scale used in the Cassini Shapiro-delay likelihood attachment: the real pulled from the §7 strong-field dataset record, equal to φ^{-44} ≈ 6.376×10^{-10}. Anyone comparing Cassini γ−1 to the RS prediction cites this constant. It is a one-line alias of the attachment field, not a derived computation.
Claim. Let $s_{\mathrm{RS}}$ be the strong-field structural target scale recorded on the §7 falsifier dataset attachment. Define the Cassini RS target scale to be that real: $s_{\mathrm{RS}} = \varphi^{-44} \approx 6.376\times 10^{-10}$.
background
The module attaches a likelihood-style certificate to the Bertotti–Iess–Tortora Cassini radio-link Shapiro-delay measurement $\gamma - 1 = (2.1 \pm 2.3)\times 10^{-5}$. Recognition Science supplies a structural strong-field target, not a free fit parameter: $\varphi^{-44}$ stored on strongFieldAttachment in the falsifier register.
In RS-native units the golden ratio $\varphi$ is the forced self-similar fixed point (forcing step T6). Negative powers of $\varphi$ set dimensionless suppression scales; here the strong-field PPN deviation target is $\varphi^{-44}$. The certificate is explicitly a consistency / non-sensitivity test: Cassini’s central value sits within $1\sigma$ of that target, yet the reported $\sigma$ is far larger than $\varphi^{-44}$ itself.
Sibling constants in the same file fix the Cassini central value and one-sigma width; the residual is the absolute gap between the central value and this target scale.
proof idea
Pure definitional alias: unfold to the rsTargetScale field of the strong-field dataset attachment record. No tactics, no lemmas, no arithmetic. Downstream positivity and comparison theorems re-unfold this name together with the attachment and discharge the inequalities by norm_num.
why it matters
Anchors every quantitative claim in the Cassini strong-field likelihood certificate. The residual is defined as $|(\gamma-1){\mathrm{central}} - s{\mathrm{RS}}|$; positivity of the target, residual $<1\sigma$, and $\sigma > s_{\mathrm{RS}}$ (non-sensitivity) all mention this scale. Those facts pack into CassiniStrongFieldLikelihoodCert and the one-statement conjunction theorem.
In the broader RS verification layer this is the concrete numerical face of the §7 strong-field falsifier row: the framework predicts a PPN deviation at $\varphi^{-44}$, and Cassini is recorded as compatible but not yet sensitive. It does not close an open forcing step (T0–T8 already fix $\varphi$ and the octave); it only wires that structural number into a dataset-specific Lean certificate with zero sorry and no new RS axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.