strongFieldObservableDistinctFromGRWitness
plain-language theorem explainer
Packages a channel-wise strong-field discriminator into the Track 6.C master-theorem hypothesis slot. For every named observational channel the RS shift is a positive rung-44 factor, unequal to pure GR's zero baseline. Anyone assembling the unconditional gravity master theorem cites this witness. Construction is a one-line structure inhabitant wiring an already-proved proposition and its proof.
Claim. A witness for the Track 6.C structure: the proposition that for every strong-field observable channel $c$, the RS observable shift satisfies $0 < \delta_{\mathrm{RS}}(c)$ and $\delta_{\mathrm{RS}}(c) \neq \delta_{\mathrm{GR}}(c)$ (with $\delta_{\mathrm{GR}} \equiv 0$), together with a proof that this proposition holds.
background
Track 6.C of the quantum-gravity master plan asks whether RS predictions for S-stars near Sgr A*, EHT shadow constraints, lunar laser ranging, and Cassini Shapiro delay differ from pure GR. This module supplies the algebraic discriminator only: the RS strong-field deviation carries the 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. Channel-by-channel phenomenology remains future work.
The master theorem exposes a structure whose fields are a proposition rs_strong_field_distinct_GR_only and a proof that it holds. The observable-channel proposition asserts: for every named channel $c$, the RS shift is strictly positive and unequal to the pure-GR shift. An upstream theorem already proves that claim by introducing $c$ and pairing the positivity lemma with the inequality-to-pure-GR lemma.
proof idea
One-line structure inhabitant. The proposition field is set to the observable-channel discriminator (forall channels, RS shift positive and unequal to pure GR). The holds field is the existing theorem that proves that proposition by intro c and pairing the per-channel positivity and inequality lemmas. No new algebra is performed here.
why it matters
Retires the Track 6.C hypothesis from the conditional gravity master theorem by inhabiting StrongFieldTestsDistinctFromGR with a channel-strengthened witness rather than a bare nonzero deviation. Downstream, the unconditional master assembly records this as the still-valid channel-route witness (canonicalStrongFieldDistinctWitness_channelRoute). The $\varphi^{-44}$ scale ties the strong-field discriminator to the same rung-44 forcing used for $\eta_B$ in the cosmology ladder, keeping gravity and cosmology on one phi-ladder. Specific observational deviation patterns per channel are still open; this closes only the structural distinctness slot.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.