pith. machine review for the scientific record. sign in
def definition def or abbrev high

alpha_s_running

show as:
view Lean formalization →

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.

claimThe 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  56def alpha_s_running (Q_GeV : ℝ) : ℝ :=

proof body

Definition body.

  57  alpha_s_MZ / (1 + beta0 N_f_Z * alpha_s_MZ * Real.log (Q_GeV ^ 2 / M_Z_GeV ^ 2) / (2 * Real.pi))
  58
  59/-- For Q < M_Z, ln(Q²/M_Z²) < 0, so α_s increases (asymptotic freedom in reverse). -/

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (6)

Lean names referenced from this declaration's body.