strongFieldObservableChannelFactor_pos
plain-language theorem explainer
For each named strong-field channel (S-stars, EHT shadow, Cassini Shapiro), the channel response factor is strictly positive. Downstream positivity of the RS observable shift multiplies this factor by the universal rung-44 deviation, so anyone citing that product needs this lemma. The proof is a three-way case split with numerical normalization on the constants 1, 2, and 3.
Claim. Let $c$ be any strong-field observable channel among S-stars near Sgr A*, the EHT shadow, and Cassini Shapiro delay. Write $f(c)$ for the channel response factor attached to $c$. Then $0 < f(c)$.
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, EHT shadow, Cassini Shapiro, and related probes). This module supplies the algebraic form: RS carries a universal positive deviation $\varphi^{-44}$ (the same rung-44 scale that forces $\eta_B = \varphi^{-44}$ on the phi-ladder), while pure GR predicts zero deviation.
The three channels are packaged as an inductive type. Each channel is assigned a positive real response factor that multiplies the universal rung-44 deviation: factor $1$ for S-stars, $2$ for the EHT shadow, and $3$ for Cassini Shapiro. The observable shift in a channel is then that factor times $\varphi^{-44}$.
Positivity of the product therefore splits into positivity of the factor and positivity of $\varphi^{-44}$. This declaration handles the factor half.
proof idea
Term-mode proof by exhaustive case analysis on the three constructors of the channel type. On each branch, unfold the factor definition and discharge $0 < 1$, $0 < 2$, and $0 < 3$ by norm_num. No external lemmas are required beyond the definition of the factor map.
why it matters
Feeds rs_strong_field_observable_shift_pos, which multiplies this factor by the positive rung-44 deviation to conclude that the RS observable shift is strictly positive in every named channel. That positivity is the concrete half of the structural discriminator: RS predicts a nonzero strong-field signature while pure GR predicts zero.
In the broader framework this sits inside Gravity Track 6.C and supports the witness that retires the master-theorem hypothesis StrongFieldTestsDistinctFromGR. The universal scale $\varphi^{-44}$ is the same rung-44 forcing that appears in the cosmology phi-ladder for $\eta_B$. Specific per-channel deviation patterns (orbital residuals, shadow diameter shifts, Shapiro delay) remain future physics work; this lemma only locks the algebraic positivity of the channel weights.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.