alpha_s_running
plain-language theorem explainer
The definition supplies the one-loop running formula for the strong coupling α_s at arbitrary scale Q in GeV, anchored at the RS value of α_s at the Z-boson mass. QCD phenomenologists and lattice gauge theorists cite it when evolving couplings from the electroweak scale to nuclear scales. The implementation is a direct algebraic substitution of the standard one-loop beta-function solution using RS-native constants for α_s(M_Z), β₀, and N_f.
Claim. The one-loop running strong coupling at scale $Q$ (in GeV) is given by $α_s(Q) = α_s(M_Z) / (1 + β_0(N_f^Z) · α_s(M_Z) · ln(Q²/M_Z²) / (2π))$, where $α_s(M_Z)$ is the Recognition Science value at the Z pole, $β_0(N_f) = (11N_c - 2N_f)/(12π)$ is the one-loop coefficient with $N_c = 3$, $N_f^Z = 5$, and $M_Z ≈ 91.1876$ GeV.
background
The module implements the one-loop running of the strong coupling α_s within the Recognition Science framework. The beta-function coefficient β₀(N_f) = (11N_c − 2N_f)/(12π) with N_c = 3 yields asymptotic freedom for N_f ≤ 16. The anchor value α_s(M_Z) is taken from the geometric RS prediction α_s_geom. Upstream, the general running formula appears in RunningCouplings.alpha_s_running as α_s(μ) = α_s(μ*) / (1 + b₀/(2π) α_s(μ*) ln(μ/μ*)). The specific constants N_f_Z = 5, M_Z_GeV = 91.1876, and beta0 are defined locally to specialize this to the Z scale.
proof idea
The definition is a direct one-line specialization of the general one-loop running formula, substituting the RS anchor α_s_MZ, the fixed N_f_Z = 5, and the beta0 coefficient evaluated at that flavor number.
why it matters
This definition supplies the concrete running law used by the theorems alpha_s_positive and rs_alpha_s_MZ_range in the RunningCouplings module. It realizes the one-loop beta-function evolution required by the Recognition Science treatment of QCD, where α_s = 2/17 at M_Z and the positive β₀ enforces asymptotic freedom. The construction closes the interface between the RS constants and standard perturbative QCD running.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.