alpha_s_running
plain-language theorem explainer
The one-loop running formula for the strong coupling α_s(μ) expresses the value at arbitrary scale μ directly from an anchor value at reference scale μ* using the beta-function coefficient b₀. QCD phenomenologists computing coupling evolution from the RS anchor would cite this definition. It is a direct algebraic transcription of the closed-form solution to the one-loop renormalization group equation.
Claim. α_s(μ) = α_s(μ*) / (1 + (b₀/(2π)) α_s(μ*) ln(μ/μ*))
background
In the Recognition Science framework the renormalization group flow for couplings is derived from the φ-ladder derivative of the coupling strength. The module states that β(g) = (1/ln φ) dg/dr, with the sign of the β-function fixed by the SU(3) color structure forced by Q₃. The RS anchor scale μ* = 182.201 GeV is a stationarity point of this flow, and asymptotic freedom holds for n_f ≤ 16 flavors.
proof idea
This is a direct definition that transcribes the analytic solution of the one-loop RG equation. No lemmas are invoked; the expression is written explicitly using Real.log and ordinary arithmetic on real numbers.
why it matters
This definition supplies the running coupling instantiated at the Z scale in rs_alpha_s_MZ and whose positivity is proved in alpha_s_positive. It fills the running_coupling_formula entry in RS_Renormalization_Running_Couplings.tex and connects the QCD beta-function sign to the φ-ladder derivative required by the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.