alpha_s_positive
plain-language theorem explainer
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.
Claim. If $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.