rs_alpha_s_MZ
plain-language theorem explainer
The RS strong coupling at the Z-pole is obtained by one-loop running of the anchor value 0.1181 from 182.201 GeV down to 91.2 GeV with the QCD beta coefficient b0 = 7 for six flavors. Phenomenologists cite it when comparing the Recognition Science prediction to the measured α_s(M_Z). The definition is a direct substitution into the one-loop running formula.
Claim. $α_s^{RS}(M_Z) := α_s(μ^*) / (1 + (b_0 α_s(μ^*) / (2π)) ln(M_Z / μ^*))$ with $b_0 = 7$, $α_s(μ^*) = 0.1181$, $μ^* = 182.201$ GeV and $M_Z = 91.2$ GeV.
background
The module treats renormalization-group evolution of couplings as a direct consequence of the φ-ladder derivative of the coupling. The anchor scale μ* = 182.201 GeV is defined as a stationarity point of the RG flow; the one-loop running formula follows from integrating β(g) = (1/ln φ) dg/dr. The coefficient b0_qcd(n_f) = 11 - 2 n_f/3 evaluates to 7 for the six active flavors of the Standard Model, guaranteeing asymptotic freedom. The upstream definition alpha_s_running implements the integrated solution α_s(μ) = α_s(μ*) / (1 + b0 α_s(μ*) ln(μ/μ*)/(2π)).
proof idea
One-line definition that applies alpha_s_running to the RS anchor value, the b0_qcd coefficient evaluated at six flavors, the numerical scale 91.2 GeV, and the anchor scale.
why it matters
This supplies the RS value of α_s at the Z pole that is consumed by the downstream theorem rs_alpha_s_MZ_range to prove the result lies in the perturbative window (0.11, 0.14). It realizes the running_coupling_formula listed in the module documentation and the paper RS_Renormalization_Running_Couplings.tex. Within the framework it shows how the φ-ladder forces the sign of the QCD beta function for n_f ≤ 16.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.