rs_strong_field_observable_shift
plain-language theorem explainer
The RS strong-field shift in a named observational channel equals a positive channel response factor times the universal rung-44 deviation φ^{-44}. Gravity and QG auditors cite it when comparing RS to pure GR on S-stars, EHT shadow, or Cassini Shapiro. The body is a one-line product of those two real factors.
Claim. For each named strong-field channel $c$ (S-stars near Sgr A*, EHT shadow, or Cassini Shapiro delay), the RS observable shift is $\mathrm{factor}(c)\cdot\varphi^{-44}$, where $\mathrm{factor}(c)>0$ is the channel response and $\varphi^{-44}$ is the universal RS strong-field deviation scale.
background
Track 6.C of the quantum-gravity master plan asks for structural discriminators on strong-field tests: S-stars near Sgr A*, EHT shadow constraints, and Cassini Shapiro delay. This module supplies the algebraic form only: RS carries a positive $\varphi$-rational signature $\varphi^{-44}$ (the same rung-44 forcing that yields $\eta_B=\varphi^{-44}$ on the phi-rung ladder), while pure GR predicts zero deviation in the same channels.
StrongFieldObservableChannel is the inductive naming those three falsifier-surface channels. Each channel has a positive response factor that multiplies the universal deviation. The sibling rs_strong_field_phi_deviation is exactly $\varphi^{-44}$. The pure-GR baseline shift in the same channel is the zero constant defined next to this declaration.
proof idea
Definition, not a proved theorem. The value is the product of the channel response factor for $c$ and the fixed RS strong-field phi-deviation $\varphi^{-44}$. No tactics or lemmas fire at this site; downstream positivity unfolds the product and multiplies the two strict positivity facts.
why it matters
This is the per-channel quantity that makes Track 6.C's structural discriminator checkable. Downstream, rs_strong_field_observable_shift_pos shows the shift is strictly positive, rs_strong_field_observable_shift_ne_pureGR shows it differs from the pure-GR zero baseline, and rs_strong_field_observable_distinct_GR_prop packages both for every named channel.
Together with the witness that retires StrongFieldTestsDistinctFromGR from the gravity master theorem hypothesis list, it closes the algebraic half of Track 6.C (module status: 0 sorry, structural theorem). The landmark is the rung-44 / $\varphi^{-44}$ scale shared with the baryon asymmetry forcing on the phi ladder. Exact deviation patterns inside each observational channel remain future physics work.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.