pureGR_strong_field_observable_shift
plain-language theorem explainer
Pure general relativity predicts zero strong-field shift in every named observable channel (S-stars, EHT shadow, Cassini Shapiro). Gravity and QG auditors cite this as the GR null baseline against which the RS rung-44 deviation is compared. It is a constant definition: the map sends every channel to the real number 0.
Claim. For every strong-field observable channel $c$ (S-stars near Sgr A*, EHT shadow, or Cassini Shapiro delay), the pure-GR baseline shift in that channel equals $0$.
background
Track 6.C of the quantum-gravity master plan asks for structural discriminators between Recognition Science and pure GR in strong-field tests: S-stars near Sgr A*, EHT shadow constraints, and Cassini Shapiro delay. This module supplies the algebraic form of that discriminator, not the full channel-by-channel physics.
Channels are named by the inductive type of strong-field observable channels (S-stars, EHT shadow, Cassini Shapiro). The RS side attaches a positive $\varphi^{-44}$ shift (the same rung-44 scale that forces $\eta_B = \varphi^{-44}$ on the cosmology ladder). Pure GR is the zero baseline in the same channels.
The definition here is that pure-GR baseline: independent of channel, the predicted shift is identically zero.
proof idea
Constant definition, not a proved theorem. The body ignores the channel argument and returns the real literal $0$. No lemmas or tactics are involved.
why it matters
This zero baseline is the pure-GR side of the observable-channel discriminator. Downstream, the inequality theorem shows the RS channel shift is unequal to this pure-GR value, and the discriminator proposition asserts that every named channel has a strictly positive RS shift distinct from the pure-GR zero.
Together with the positive $\varphi^{-44}$ RS deviation, it closes the structural half of Track 6.C: RS carries a positive $\varphi$-rational signature while pure GR predicts none. That witness retires the master-theorem hypothesis that strong-field tests are distinct from GR. Exact per-channel deviation patterns remain future physics work; only the algebraic null baseline is fixed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.