rs_strong_field_observable_shift_ne_pureGR
plain-language theorem explainer
For every named strong-field observable channel (S-stars, EHT shadow, Cassini Shapiro), the RS predicted shift differs from the pure-GR baseline shift. Anyone citing Track 6.C structural discriminators or the Gravity master-theorem witness needs this inequality. The proof is a short positivity contradiction: the RS channel shift is strictly positive while pure GR is identically zero.
Claim. For every strong-field observable channel $c$ (S-stars near Sgr A*, EHT shadow, or Cassini Shapiro delay), the Recognition Science channel shift is unequal to the pure general-relativity channel shift: $\mathrm{shift}_{\mathrm{RS}}(c) \neq \mathrm{shift}_{\mathrm{GR}}(c)$.
background
Track 6.C of the quantum-gravity master plan asks for structural strong-field discriminators against pure GR in named observational channels: S-stars, EHT shadow, and Cassini Shapiro. This module supplies the algebraic form of that discriminator, not the full channel-by-channel phenomenology.
The universal RS strong-field deviation scale is $\varphi^{-44}$, the same rung-44 forcing that appears as $\eta_B = \varphi^{-44}$ on the cosmology phi-rung ladder. Each StrongFieldObservableChannel multiplies that scale by a positive channel response factor, yielding a channel-dependent RS shift. Pure GR is assigned the zero baseline shift in every channel.
The sibling positivity lemma already shows the RS channel shift is strictly positive. The present statement only needs the comparison to the pure-GR zero map.
proof idea
Term-mode proof by contradiction. Assume the RS channel shift equals the pure-GR channel shift. Invoke the sibling positivity theorem that the RS shift is strictly positive. Unfold the pure-GR shift definition (identically zero) and rewrite the positivity hypothesis under the assumed equality. linarith then derives the contradiction $0 < 0$.
why it matters
This inequality is half of the per-channel structural discriminator. Its sole downstream consumer packages it with positivity into rs_strong_field_observable_distinct_GR_prop_holds, which states that every named channel receives a positive rung-44 RS shift and is therefore distinct from pure GR's zero baseline.
That package feeds the witness inhabiting StrongFieldTestsDistinctFromGR on the Gravity master theorem, retiring Track 6.C from the conditional hypothesis list. Framework-wise it is the strong-field face of the same $\varphi^{-44}$ rung forcing used in cosmology; it does not yet derive numerical residuals for S-stars, EHT, or Cassini, which remain future physics work on top of this algebraic spine.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.