gammaMassQCD1L_zero
plain-language theorem explainer
The declaration establishes that the minimal one-loop QCD mass anomalous dimension vanishes at zero strong coupling. It would be cited in derivations of the integrated mass residue when the renormalization scale reaches an infrared fixed point. The proof is a one-line term-mode simplification that unfolds the explicit definition and reduces the product to zero by arithmetic.
Claim. Let $γ_m(α_s) := (2/π) α_s$ denote the one-loop mass anomalous dimension scaffold for QCD. Then $γ_m(0) = 0$.
background
The module formalizes renormalization-group transport of mass residues. Fermion masses run with scale μ according to d(ln m)/d(ln μ) = -γ_m(μ), and the integrated residue f(μ₀, μ₁) = (1/λ) ∫ γ_m(μ') d(ln μ') enters the structural mass relation m(μ⋆) = m_phys · φ^{f}. The function gammaMassQCD1L supplies the minimal one-loop scaffold γ_m(α_s) = (2/π) α_s for the strong sector, with exact higher-loop expressions left to Level-B extensions.
proof idea
The proof is a one-line term-mode wrapper that applies simp to the definition of gammaMassQCD1L, substituting the explicit formula (2 / Real.pi) * alphaS and evaluating the product at zero.
why it matters
This anchors the RG transport module by confirming the expected vanishing at zero coupling, consistent with the mass formula that relates structural and physical masses via the phi-ladder. It supports integrated residue calculations that connect to the Recognition Science yardstick * phi^(rung - 8 + gap(Z)). No downstream uses are recorded, leaving open its integration into full QCD kernels.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.