betaQCD1L
plain-language theorem explainer
betaQCD1L encodes the one-loop QCD beta function as beta(alpha_s) = -(beta0(nf)/(2 pi)) alpha_s^2. Particle physicists computing running couplings or mass residues at one loop would cite this when integrating the RG flow for alpha_s. The definition is a direct algebraic expression that pulls the leading coefficient from beta0QCDReal.
Claim. $β_{QCD}^{1L}(n_f, α_s) = - (β_0(n_f) / (2 π)) α_s^2$
background
The RGTransport module formalizes renormalization-group transport that defines the empirical mass residue f^exp. Fermion masses run with scale μ via d(ln m)/d(ln μ) = -γ_m(μ), and the integrated residue enters the structural mass formula at the φ-ladder anchor. beta0QCDReal supplies the real-valued leading coefficient β_0(n_f) that appears in the one-loop beta function for the strong coupling.
proof idea
Direct definition implementing the standard one-loop formula by scaling the imported beta0QCDReal coefficient by the quadratic term in alphaS.
why it matters
This definition supplies the explicit one-loop QCD beta function inside the RGTransport module, enabling the connection from running couplings to mass residues. It is invoked by the downstream vanishing theorem betaQCD1L_vanishes_at_zero and supports the integrated anomalous-dimension formula that links to the Recognition Science mass ladder. It fills the one-loop kernel slot within the broader RG transport framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.