sStarCorrectionValue_pos
plain-language theorem explainer
The S-star periapsis correction φ^(-s), with s the strong-field rung, is strictly positive. Gravity and QG-channel authors cite it when packaging the S-star residual as a DerivedChannelPrediction. The proof is a one-line wrapper: integer powers of φ stay positive because φ > 0.
Claim. The S-star periapsis timing residual correction $\varphi^{-s}$ is strictly positive, where $s$ is the strong-field rung and $\varphi$ is the golden ratio.
background
This module derives φ-power corrections for five quantum-gravity falsifier channels from the rung address of each observable. The substrate assigns rung $r(L)=\log_\varphi(L/\ell_{\mathrm{sub}})$ to length scale $L$; recognition corrections at rung $r$ scale as $\varphi^{-r}$.
The strong-field rung $s$ is fixed at 44: half the horizon information of an astrophysical black hole is processed there, and the same rung appears in the baryon asymmetry $\eta_B=\varphi^{-44}$. The S-star channel samples that rung directly: the periapsis timing residual near Sgr A* is predicted to be $\varphi^{-s}$.
Upstream, sStarCorrectionValue is defined as $\varphi^{-\mathrm{strongFieldRung}}$. The constant $\varphi$ is positive by the RS constants layer, so integer powers remain positive.
proof idea
One-line wrapper. Apply Mathlib's zpow_pos to the hypothesis that $\varphi>0$ (from the constants module). The exponent is immaterial: any integer power of a positive real is positive. No channel-specific algebra is needed.
why it matters
Feeds sStarDerived, which packages the S-star periapsis channel as a DerivedChannelPrediction with rung 44, geometric prefactor 1, and this correction value. Without positivity, the derived prediction record would not be a well-formed positive residual scale.
In the module table, S-star sits beside PTA ($\varphi^{-44}$), EHT ($2\varphi^{-44}$), Cassini ($3\varphi^{-44}$), and ringdown ($\varphi^{-1}$). Positivity of the bare $\varphi$-power is the shared arithmetic fact that lets each channel's derived record close. The structural link to T6 ($\varphi$ as self-similar fixed point) and the shared rung-44 coincidence with $\eta_B$ is inherited from the module setting, not reproved here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.