rs_strong_field_observable_distinct_GR_prop
plain-language theorem explainer
Defines the observable-channel strong-field discriminator: for every named channel (S-stars, EHT shadow, Cassini Shapiro), the RS shift is strictly positive and unequal to the pure-GR baseline of zero. Gravity and QG auditors cite it when packaging Track 6.C into the master-theorem witness. The body is a pure Prop abbreviation over the channel type and the two shift maps.
Claim. For every strong-field observable channel $c$ (S-stars near Sgr A*, EHT shadow, or Cassini Shapiro delay), the RS channel shift is strictly positive and differs from the pure-GR channel shift: $0 < \delta_{\mathrm{RS}}(c)$ and $\delta_{\mathrm{RS}}(c) \neq \delta_{\mathrm{GR}}(c)$, where $\delta_{\mathrm{GR}}(c) = 0$ and $\delta_{\mathrm{RS}}(c)$ is the channel factor times the rung-44 scale $\varphi^{-44}$.
background
Track 6.C of the quantum-gravity master plan asks for structural discriminators on strong-field tests (S-stars, EHT shadow, Cassini Shapiro, etc.). 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 cosmology phi-rung ladder), while pure GR predicts zero deviation.
The named channels are the inductive type with constructors for S-stars, EHT shadow, and Cassini Shapiro. The RS observable shift on a channel is the product of a positive channel factor and the structural deviation $\varphi^{-44}$. The pure-GR baseline shift is the constant zero map on the same channels.
The proposition packages the per-channel claim that the RS shift is positive and unequal to that zero baseline, so the discriminator is channel-indexed rather than a single bare nonzero scalar.
proof idea
Definitional Prop, not a proved theorem. The body is the universal quantification over channels of the conjunction "RS shift positive and RS shift unequal to pure-GR shift." No tactics or lemmas fire here; discharge happens downstream in the companion theorem that intro's the channel and applies the positivity and inequality lemmas for the observable shift.
why it matters
Closes the observable-channel strengthening of Track 6.C's structural discriminator. Downstream, the holds theorem proves this Prop, and the master-theorem witness packages it as the rs_strong_field_distinct_GR_only field of StrongFieldTestsDistinctFromGR, retiring that hypothesis from the conditional gravity master theorem.
The rung-44 scale ties the gravity discriminator to the same $\varphi$-ladder forcing used for $\eta_B$ in cosmology. Specific per-channel deviation patterns (exact S-star residuals, shadow radius shifts, Shapiro delay) remain future physics work; this object only locks the algebraic nonzero signature against pure GR's zero baseline.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.