alpha_s_running
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 in Recognition Science
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.
scope and limits
- Does not include two-loop or higher corrections to the beta function.
- Does not derive b₀ from the φ-ladder; that is supplied separately by b0_qcd.
- Does not address non-perturbative effects below the anchor scale.
- Does not compute the running of electromagnetic or weak couplings.
Lean usage
rs_alpha_s_MZ : ℝ := alpha_s_running rs_alpha_s_anchor (b0_qcd 6) 91.2 rs_anchor_scaleformal statement (Lean)
82noncomputable def alpha_s_running (α_s_anchor b₀ μ μ_star : ℝ) : ℝ :=
proof body
Definition body.
83 α_s_anchor / (1 + b₀ / (2 * Real.pi) * α_s_anchor * Real.log (μ / μ_star))
84
85/-- α_s is positive when denominator is positive. -/