alpha_s_running
plain-language theorem explainer
The definition supplies the standard one-loop formula for the strong coupling α_s at scale μ given an anchor value at μ*. Physicists working on QCD running couplings would cite it when deriving RS-specific values at M_Z. It is a direct algebraic transcription of the integrated one-loop beta-function solution. The formula appears verbatim in the module doc-comment as the running_coupling_formula. Downstream definitions such as rs_alpha_s_MZ apply it with the RS anchor scale and b0_qcd 6.
Claim. $\alpha_s(\mu) = \frac{\alpha_s(\mu^*)}{1 + \frac{b_0}{2\pi} \alpha_s(\mu^*) \ln(\mu / \mu^*)}$ where $\mu^*$ is the RS anchor scale, $b_0$ is the one-loop coefficient, and the expression follows from integrating the beta function.
background
The module treats renormalization-group flow as a consequence of the RS φ-ladder. The anchor scale μ* = 182.201 GeV is defined as a stationarity point of the RG flow. The beta function is obtained from the ladder derivative: β(g) = (1/ln φ) dg/dr. Asymptotic freedom follows for n_f ≤ 16 flavors from the sign of this derivative under the SU(3) structure forced by Q3.
The upstream definition in QCDRGE.AlphaRunning supplies an equivalent one-loop expression but parameterized by Q_GeV and M_Z; the present definition generalizes it to arbitrary anchor and scale. The module doc-comment states: 'The RS anchor scale μ* = 182.201 GeV is a stationarity point of the RG flow.'
proof idea
One-line definition that transcribes the integrated one-loop beta-function solution. No lemmas are applied; the body is the closed-form expression given in the doc-comment.
why it matters
This supplies the running_coupling_formula referenced in the module doc-comment and is the direct parent of rs_alpha_s_MZ and rs_alpha_s_MZ_range. The latter proves the one-loop RS value at M_Z lies in (0.11, 0.14). It implements the RG flow whose sign is fixed by the φ-ladder derivative (T6 self-similar fixed point and T7 eight-tick octave). The definition closes the interface between the abstract ladder and concrete QCD observables.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.