cassiniDerived
plain-language theorem explainer
Packages the Cassini Shapiro-delay residual as a derived QG-channel prediction at rung 44 with geometric prefactor 3, so the correction equals $3\varphi^{-44}$. Gravity auditors cite it when building the five-channel list or the shared-rung-44 certificate. The equality field is discharged by unfolding the correction definition and ringing; positivity is inherited from the sibling positivity lemma.
Claim. The Cassini/Shapiro-delay channel is the derived prediction whose observable is the residual $\delta\Delta t/\Delta t$, whose rung is $r=44$, whose geometric prefactor is $3$, and whose correction value equals $3\,\varphi^{-44}$ and is strictly positive.
background
This module derives $\varphi$-powers for quantum-gravity falsifier channels from the rung scale address of each observable. The substrate assigns $r(L)=\log_\varphi(L/\ell_{\mathrm{sub}})$; corrections at rung $r$ scale as $\varphi^{-r}$.
The strong-field rung is fixed at $44$: half the horizon-area rung for stellar-mass black holes ($A/\ell_{\mathrm{sub}}^2\approx\varphi^{88}$), and the same address as the baryon asymmetry $|\eta_B|=\varphi^{-44}$. Cassini is the Shapiro-delay residual along a radio path past the Sun (or analogous strong-field mass).
DerivedChannelPrediction packages channel name, observable string, integer rung, real geometric prefactor, the numerical correction, a proof that correction equals prefactor times $\varphi^{-\mathrm{rung}}$, and positivity. The Cassini correction value is defined as $3\cdot\varphi^{-\mathrm{strongFieldRung}}$, the factor $3$ from three accumulated rung crossings on the line of sight (ingress, closest approach, egress).
proof idea
Structure instance, not a tactic proof of a Prop. Fields are filled literally: name and observable strings, rung $44$, prefactor $3$, and correctionValue pointed at the sibling cassiniCorrectionValue.
The equality obligation correctionValue = 3 * phi^(-rung) is a one-line wrapper: unfold cassiniCorrectionValue and strongFieldRung, then ring. Positivity is the already-proved cassiniCorrectionValue_pos (product of a positive numeral and a positive $\varphi$-power).
why it matters
Fills the Cassini row of the module table: correction $3\cdot\varphi^{-44}$ from path-integral geometry on the strong-field rung. Downstream it is the fourth entry of derivedChannels, supplies the fourth conjunct of four_channels_share_rung_44, and is required by the master certificate QGChannelRungDerivationCert (five channels, all positive, four at rung 44).
In the Recognition framework this is a concrete gravity-side use of the $\varphi$-ladder and the structural coincidence that strong-field GW injection and $\eta_B$ share rung 44. It does not invent a new rung; it only attaches the geometric prefactor $3$ forced by the delay integral.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.