strongFieldObservableChannelFactor
plain-language theorem explainer
Assigns positive integer response weights 1, 2, 3 to the three named strong-field channels (S-stars, EHT shadow, Cassini Shapiro). Anyone building channel-dependent RS observable shifts multiplies the universal rung-44 deviation by this factor. The definition is a pure case split on the channel inductive.
Claim. A map from strong-field observable channels to $\mathbb{R}$ sending the S-star channel to $1$, the EHT shadow channel to $2$, and the Cassini Shapiro-delay channel to $3$. These are the channel response factors that multiply the universal rung-$44$ RS deviation $\varphi^{-44}$.
background
Track 6.C of the quantum-gravity master plan asks for structural discriminators among strong-field tests: S-stars near Sgr A*, EHT shadow constraints, and Cassini Shapiro delay. The module supplies the algebraic skeleton only: RS carries a universal positive deviation $\varphi^{-44}$ (the same rung-44 scale that forces $\eta_B = \varphi^{-44}$ on the phi-rung ladder), while pure GR predicts zero.
The inductive StrongFieldObservableChannel names the three channels on the QG falsifier surface. The present definition attaches a fixed positive real weight to each name. Downstream, the RS observable shift in a channel is exactly this weight times the universal $\varphi^{-44}$ deviation; pure GR keeps a zero baseline in every channel.
proof idea
Definition by exhaustive pattern match on the three constructors of the channel inductive. No lemmas, no tactics: S-stars maps to $1$, EHT shadow to $2$, Cassini Shapiro to $3$.
why it matters
Gives the channel-dependent prefactor that turns the single structural deviation $\varphi^{-44}$ into a per-channel RS observable shift. The shift definition multiplies this factor by rs_strong_field_phi_deviation; the companion positivity theorem proves every factor is strictly positive by case analysis and norm_num. Together they feed the structural discriminator that pure GR predicts zero shift while RS predicts a positive $\varphi$-rational pattern, discharging the master-theorem hypothesis StrongFieldTestsDistinctFromGR. Exact numerical deviation patterns per channel remain future physics work; this object only locks the algebraic weights.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.