running_ratio
plain-language theorem explainer
The running ratio is α⁻¹(M_Z)/α⁻¹(0): PDG inverse fine structure at the Z pole over the RS-native value at vanishing momentum. VEV and electroweak mass arguments cite it to rescale tree-level α(0) predictions to the physical scale. It is a one-line real quotient of two named constants, not a derived bound.
Claim. Define the running ratio $r = \alpha^{-1}(M_Z)/\alpha^{-1}(0)$, where $\alpha^{-1}(M_Z) = 127.951$ is the PDG central value and $\alpha^{-1}(0)$ is the Recognition Science prediction (the constant $\alpha^{-1}$ forced into the band $(137.030, 137.039)$).
background
QED running of the fine-structure constant from $q^2=0$ to $q^2=M_Z^2$ is the dominant radiative correction to electroweak mass predictions. Recognition Science fixes $\alpha^{-1}(0)$ in $(137.030, 137.039)$ from the forcing chain; the PDG reports $\alpha^{-1}(M_Z)=127.951\pm 0.009$. Their quotient is therefore expected near $(0.933, 0.935)$.
In this module, $\alpha^{-1}(0)$ is the RS constant alphaInv, and $\alpha^{-1}(M_Z)$ is the fixed empirical check value $127.951$ (not an RS input). The same ratio appears in the VEV-consistency layer as the factor that corrects the tree-level vacuum expectation value to the physical scale. The module's larger claim is that the correction is calculable from RS-derived particle content (three charged leptons, five light quarks, plus $W$), with zero extra free parameters.
proof idea
Pure definition: the real number equal to the quotient of the PDG inverse-alpha at $M_Z$ by the RS inverse-alpha at zero. No tactics, no lemmas. Downstream inequality proofs unfold this name and rewrite the comparison as a product inequality against the known $\alpha^{-1}(0)$ band bounds.
why it matters
This name is the shared handle for the alpha-running scorecard and the VEV consistency certificate. The scorecard bundles the ratio band $(0.933, 0.935)$, the inequality $r<1$, the RS $\alpha^{-1}(0)$ band, and the particle-content counts (3 leptons, 5 light quarks) to show the correction is not fitted. VEVConsistency uses an analogous ratio to prove the corrected vacuum expectation value lands in the PDG range from RS inputs alone.
In the framework, $\alpha^{-1}(0)$ is a landmark output of the forcing chain (the narrow band around $137$). The running ratio converts that zero-momentum prediction into the electroweak scale without introducing a new free parameter, which is exactly what the scorecard's zero-free-params claim records.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.