cassiniChannel
plain-language theorem explainer
Cassini/Shapiro delay residual as a typed QG falsifier channel: RS predicts fractional residual $3\varphi^{-44}$ beyond standard PPN, GR predicts zero. Cited by the five-channel list and the strong-field distinctness witness. Definition packages the numbers with elementary positivity proofs that the residual is nonzero and positively separated from the GR baseline.
Claim. The Cassini/Shapiro observation channel is the typed signal model whose observable is the Shapiro delay residual $\delta\Delta t/\Delta t$, whose RS prediction is $3\varphi^{-44}$, and whose null (GR) baseline is $0$, together with proofs that the prediction differs from the baseline and that $|\mathrm{RS}-\mathrm{null}|>0$.
background
This module builds typed observation-channel signal models for the D5 quantum-gravity falsifier surface. Status is structural (zero sorry, zero RS-internal axiom). Each channel carries a named observable, an RS prediction, a GR/ΛCDM null baseline, and proofs that the two values are unequal and positively separated.
ObservationChannelSignalModel is the carrier structure: string labels for channel and observable, real rsPrediction and nullBaseline, plus the two separation obligations rsPrediction ≠ nullBaseline and $0 < |rsPrediction - nullBaseline|$. The five channels are PTA stochastic background, EHT shadow/ring, S-star orbits near Sgr A*, Cassini/Shapiro delay, and ringdown echoes.
Here the physical content is the Cassini radio-link Shapiro time delay. Standard PPN GR predicts a definite delay; RS asserts a positive fractional residual beyond that parametrization, scaled by $3\varphi^{-44}$ with $\varphi$ the golden-ratio fixed point from the forcing chain (T6). The null baseline is exactly zero residual.
proof idea
Structure instance, not a deep theorem. The two proof fields are short positivity arguments.
rsPrediction_ne_null: assume $3\varphi^{-44}=0$; zpow_pos phi_pos (-44) gives $\varphi^{-44}>0$, so the product with 3 cannot vanish; linarith closes.
separation_pos: build $0 < 3\varphi^{-44}$ by mul_pos on norm_num for the factor 3 and zpow_pos for the power; rewrite $|x-0|$ via sub_zero and abs_of_pos, then return the same positivity fact.
why it matters
Fills the Cassini/Shapiro slot in the five-channel QG falsifier matrix described by the module doc. Downstream, qgChannels collects it with PTA, EHT, S-star, and ringdown into the canonical list. strongFieldSignalModelWitness uses cassiniChannel.rsPrediction ≠ cassiniChannel.nullBaseline as one conjunct of the strong-field distinctness claim (RS strong-field tests distinct from GR-only baselines), alongside EHT and S-star.
In the broader RS gravity program this is a concrete, numerically tiny but strictly positive deviation from classical GR in a solar-system timing observable, complementary to the strong-field imaging and stellar-orbit channels. It does not itself invoke T5–T8 or the RCL; it consumes $\varphi$ as an already-forced constant and records the channel-level prediction for later experimental comparison.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.