alpha_s_positive
Positivity of the one-loop running strong coupling follows when the anchor value at the RS stationarity scale is positive and the denominator in the RG formula remains positive. QCD phenomenologists and Recognition Science modelers cite the result to certify that the coupling stays positive throughout the perturbative regime. The proof is a direct one-line wrapper that unfolds the running formula and invokes positivity of division on the two supplied hypotheses.
claimIf $0 < α_s(μ_*)$ and $0 < 1 + (b_0/(2π)) α_s(μ_*) log(μ/μ_*)$, then $0 < α_s(μ)$, where the running coupling is defined by the one-loop formula $α_s(μ) = α_s(μ_*) / (1 + (b_0/(2π)) α_s(μ_*) log(μ/μ_*))$.
background
The module treats renormalization-group flow as a direct consequence of the φ-ladder derivative of the coupling. The RS anchor scale μ* = 182.201 GeV is the stationarity point of this flow, and the sign of the β-function is fixed by the ladder derivative: β(g) = (1/ln φ) dg/dr. Asymptotic freedom for QCD then follows from the SU(3) gauge structure forced by the underlying spectral data.
proof idea
The proof is a one-line wrapper. It unfolds the definition of the running coupling to expose the explicit division of the anchor value by the denominator, then applies the lemma div_pos to the two positivity hypotheses on the numerator and denominator.
why it matters in Recognition Science
The result supplies the positivity field required by the StrongCouplingCert construction in Constants.StrongCoupling, where positive := alpha_s_positive appears alongside gauge-structure and boundedness certificates. It completes the running_coupling_formula entry in the RS_Renormalization_Running_Couplings paper and supports the asymptotic-freedom claim for n_f ≤ 16 flavors that follows from the φ-ladder and the Q3-forced gauge content.
scope and limits
- Does not compute or constrain the numerical value of the one-loop coefficient b0.
- Does not address two-loop or higher-order corrections to the beta function.
- Does not specify the interval of μ over which the one-loop formula remains valid.
- Does not treat non-perturbative regimes below the confinement scale.
formal statement (Lean)
86theorem alpha_s_positive (α_s_anchor b₀ μ μ_star : ℝ)
87 (hα : 0 < α_s_anchor)
88 (hdenom : 0 < 1 + b₀ / (2 * Real.pi) * α_s_anchor * Real.log (μ / μ_star)) :
89 0 < alpha_s_running α_s_anchor b₀ μ μ_star := by
proof body
Term-mode proof.
90 unfold alpha_s_running
91 exact div_pos hα hdenom
92
93/-- **RS ANCHOR SCALE**: μ* = 182.201 GeV (stationarity point of RG). -/