sStarChannel
plain-language theorem explainer
Packages the S-star periapsis channel near Sgr A* as a typed QG signal model: RS predicts a positive timing residual at scale φ^{-44}, while GR's residual beyond accounted PN terms is zero. Gravity and strong-field auditors cite it when assembling the five-channel falsifier surface. The body is a structure instance with two short positivity proofs from φ > 0.
Claim. The S-star observation channel is the typed signal model with name "S-star periapsis", observable equal to the periapsis timing residual $\delta t/P$ near Sgr A*, RS prediction $\varphi^{-44}$, and null (GR) baseline $0$, together with proofs that $\varphi^{-44} \neq 0$ and $0 < |\varphi^{-44} - 0|$.
background
This module builds typed observation-channel signal models for the D5 quantum-gravity falsifier surface. Each channel carries a measured observable, an RS prediction, a GR/ΛCDM null baseline, and proofs that the two values are distinct and positively separated.
ObservationChannelSignalModel is the common structure: string labels for channel and observable, real rsPrediction and nullBaseline, plus rsPrediction_ne_null and separation_pos. The five channels are PTA, EHT shadow/ring, S-star orbits, Cassini/Shapiro delay, and ringdown echoes.
Here the S-star channel targets periapsis timing residuals of stars orbiting Sgr A*. RS places a positive residual at the rung-44 scale $\varphi^{-44}$ (with $\varphi$ the golden ratio fixed by the self-similar fixed point in the forcing chain). GR predicts zero residual once 1PN and 2PN corrections are removed. The golden-ratio power uses the standard positivity of $\varphi$.
proof idea
A structure instance, not a deep theorem. Fields are filled directly: prediction $\varphi^{-44}$, baseline $0$.
rsPrediction_ne_null assumes equality to zero and contradicts zpow_pos phi_pos (-44), which gives $\varphi^{-44} > 0$, then closes by linarith.
separation_pos simplifies $|\varphi^{-44} - 0|$ via sub_zero and abs_of_pos on the same positivity fact, then returns that positive quantity. No external channel lemmas are required beyond phi_pos and integer power positivity.
why it matters
Fills the S-star slot in the five-channel QG falsifier matrix for strong-field gravity near the Galactic center. It is listed in qgChannels beside PTA, EHT, Cassini, and ringdown, and supplies one conjunct of strongFieldSignalModelWitness: every named strong-field channel has a positive RS deviation distinct from the GR zero baseline.
In the broader framework this is a concrete rung-44 timing residual on the $\varphi$-ladder, complementary to the EHT shadow/ring and Cassini delay channels. It does not derive $\varphi^{-44}$ from first principles inside this file; it records the structural prediction so MasterTheorem-style strong-field distinctness from GR can be stated as a typed witness rather than prose.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.