cassiniCorrectionValue_pos
plain-language theorem explainer
The Cassini Shapiro-delay residual 3·φ^(-44) is strictly positive. Gravity-channel packaging cites this to discharge the positivity field on the derived Cassini prediction. Proof is a one-line wrapper: product of two positive reals (the prefactor 3 and a positive power of φ).
Claim. Let $\varphi$ be the golden ratio and let $s$ be the strong-field rung. The Cassini correction $3\,\varphi^{-s}$ satisfies $0 < 3\,\varphi^{-s}$.
background
This module derives φ-power corrections for five quantum-gravity falsifier channels from the rung address of each observable. A length scale $L$ sits at rung $r(L)=\log_\varphi(L/\ell_{\mathrm{sub}})$; recognition corrections scale as $\varphi^{-r}$ relative to the Planck value.
The strong-field rung $s=44$ is fixed by horizon cell counting for astrophysical black holes (half-area information processing). It coincides with the baryon-asymmetry rung $\eta_B=\varphi^{-44}$. The Cassini channel is the Shapiro time-delay residual along a radio path past the Sun; the module sets its correction to $3,\varphi^{-s}$, the factor 3 coming from three accumulated rung crossings in the line-of-sight integral (ingress, closest approach, egress).
Sibling positivity lemmas exist for the PTA, EHT, S-star, and ringdown channels under the same pattern.
proof idea
One-line wrapper on the real product rule for positivity. Unfold the definition $3\cdot\varphi^{-s}$. The first factor is positive by norm_num on the literal 3. The second factor $\varphi^{-s}$ is positive by zpow_pos applied to the standing fact $\varphi>0$. No channel-specific algebra is needed beyond the definition.
why it matters
Feeds cassiniDerived, which packages the Cassini/Shapiro channel as a DerivedChannelPrediction with rung 44, geometric prefactor 3, and this correction value. That record is one of the five D5 QG-channel predictions the module exports (PTA, EHT, S-star, Cassini, ringdown).
Within Recognition Science the claim sits on the φ-ladder and the strong-field rung coincidence with $\eta_B=\varphi^{-44}$. It does not invoke the forcing chain T0–T8 directly, but it inherits φ from T6 and the discrete rung arithmetic from the eight-tick/octave structure. Closing positivity here keeps the Cassini entry on the same footing as the other channel corrections before any numerical comparison to spacecraft data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.