running_ratio_lt
plain-language theorem explainer
The QED running ratio α⁻¹(M_Z)/α⁻¹(0) is strictly less than 0.935. Anyone checking the RS alpha-running scorecard against the PDG M_Z value cites this bound. The proof unfolds the ratio, clears the positive denominator via the RS lower bound α⁻¹(0) > 137.030, and finishes by decimal arithmetic.
Claim. The running ratio $\alpha^{-1}(M_Z)/\alpha^{-1}(0)$ satisfies $\alpha^{-1}(M_Z)/\alpha^{-1}(0) < 0.935$, where $\alpha^{-1}(M_Z)$ is the PDG central value $127.951$ and $\alpha^{-1}(0)$ is the RS infrared inverse fine-structure constant.
background
This module treats the QED running of the fine-structure constant from $q^2=0$ to $q^2=M_Z^2$ as the dominant radiative correction to electroweak mass predictions. Recognition Science forces $\alpha^{-1}(0)\in(137.030,137.039)$ from the forcing chain; the PDG reports $\alpha^{-1}(M_Z)=127.951\pm 0.009$, so the ratio band is $(0.933,0.935)$.
The running ratio is the quotient of the fixed PDG central value at the Z pole by the RS infrared $\alpha^{-1}(0)$ (the assembled constant alphaInv, with lower bound from the numerics interval package). The correction itself is not a free parameter: it is fixed by the particle content below $M_Z$ (three charged leptons, five light quarks, and the W), via the one-loop vacuum-polarization sum.
Upstream, the positivity/lower bound $\alpha^{-1}(0)>137.030$ supplies the strict inequality direction needed to clear the denominator.
proof idea
Unfold the running ratio into the PDG $M_Z$ inverse-alpha over the RS infrared inverse-alpha. Rewrite the target inequality by multiplying through by the positive denominator, using the numeric lower bound on $\alpha^{-1}(0)$. Then compare: $0.935\cdot\alpha^{-1}(0)>0.935\cdot 137.030=128.12305>127.951$, so the PDG numerator sits strictly below the scaled lower bound. All steps are nlinarith/norm_num after the rewrite.
why it matters
Feeds the scorecard certificate alphaRunningCorrectionScoreCardCert_holds, which packages the $\alpha(0)$ band, the ratio band $\langle$lower, upper$\rangle$, and the particle-content counts into a single nonempty certificate. The upper edge $0.935$ is exactly the module's stated PDG-implied ceiling for $\alpha^{-1}(M_Z)/\alpha^{-1}(0)$.
In the broader RS picture this closes the claim that the running correction is calculable from RS-derived content (no extra free parameters), so the corrected VEV from RS-native $\alpha(0)$ can be checked against the PDG band. It sits downstream of the forced infrared $\alpha^{-1}$ band from the forcing chain and the alpha numerics bounds; the exact CODATA infrared pin remains an open boundary condition elsewhere, but this lemma only needs the strict lower edge $137.030$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.