rs_strong_field_observable_shift_pos
plain-language theorem explainer
For every named strong-field channel (S-stars, EHT shadow, Cassini Shapiro), the RS observable shift is strictly positive. Anyone citing the structural discriminator against pure GR needs this positivity. The proof unfolds the product definition and multiplies two already-proved positive factors.
Claim. For every strong-field observable channel $c$ among $\{$S-stars, EHT shadow, Cassini Shapiro$\}$, the RS observable shift satisfies $0 < f(c)\,\varphi^{-44}$, where $f(c)>0$ is the channel response factor and $\varphi^{-44}$ is the universal rung-44 deviation scale.
background
Track 6.C of the quantum-gravity master plan asks for a structural discriminator between RS and pure GR in strong-field tests (S-stars near Sgr A*, EHT shadow, Cassini Shapiro delay). This module supplies the algebraic form only: RS carries a positive $\varphi$-rational signature at rung 44, the same forcing scale that yields $\eta_B = \varphi^{-44}$ on the cosmology ladder, while pure GR predicts zero deviation.
The universal deviation is rs_strong_field_phi_deviation $:= \varphi^{-44}$. Each named channel multiplies that scale by a positive response factor strongFieldObservableChannelFactor. The observable shift is exactly that product. Upstream, rs_strong_field_phi_deviation_pos already gives $0 < \varphi^{-44}$ via positivity of $\varphi$ under integer powers, and strongFieldObservableChannelFactor_pos gives $0 < f(c)$ by case analysis on the three constructors.
proof idea
One-line term proof after a single unfold. Expand the observable shift to $f(c)\cdot\varphi^{-44}$. Apply the real-product positivity lemma to the pair (strongFieldObservableChannelFactor_pos c, rs_strong_field_phi_deviation_pos). Both factors are already strict inequalities, so the product is strict.
why it matters
This is the positivity half of the per-channel discriminator. Downstream, rs_strong_field_observable_shift_ne_pureGR uses it to show the RS shift differs from the pure-GR baseline (which is identically zero), and rs_strong_field_observable_distinct_GR_prop_holds packages both facts into the structural proposition that every channel has a positive RS shift unequal to pure GR.
That package inhabits the master-theorem hypothesis StrongFieldTestsDistinctFromGR, retiring it from the conditional gravity master theorem. Framework landmark: the rung-44 scale $\varphi^{-44}$ is the same forcing that appears as $\eta_B$ on the $\varphi$-ladder. The module is closed (0 sorry); the remaining open work is deriving the concrete deviation pattern in each observational channel, not the algebraic sign.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.