gammaMassQCD1L
plain-language theorem explainer
The definition supplies the leading one-loop QCD mass anomalous dimension as (2/π)α_s for use in RG-integrated mass residues. Recognition Science mass-formula work cites it when constructing the empirical residue f^exp from the structural anchor scale. The body is a direct algebraic assignment with no reduction steps.
Claim. The one-loop QCD mass anomalous dimension is defined by $γ_m^{QCD,1L}(α_s) = (2/π) α_s$.
background
The RGTransport module formalizes renormalization-group transport of mass residues. Fermion masses run according to d(ln m)/d(ln μ) = -γ_m(μ), and the integrated residue is f(μ₀, μ₁) = (1/λ) ∫ γ_m d(ln μ) with λ = ln φ. This residue converts the structural mass at the anchor scale μ⋆ into the physical mass via m_phys = m_struct · φ^{-f}.
proof idea
The definition is a one-line wrapper that directly returns the expression (2 / Real.pi) * alphaS using only real arithmetic.
why it matters
It supplies the QCD one-loop term required by the downstream theorem gammaMassQCD1L_zero and by the RG transport that defines f^exp in the mass formula. The module doc-comment notes that exact higher-loop kernels are deferred to Level-B extensions. Within the framework it links the phi-ladder mass formula to the running of α_s.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.