gammaMassQCD1L_zero
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.
claimLet $γ_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 in Recognition Science
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.
scope and limits
- Does not incorporate scheme-dependent higher-loop contributions to the anomalous dimension.
- Does not compute the integrated transport integral for the residue f.
- Does not address QED or mixed coupling effects.
- Does not derive the beta function or running of alpha_s itself.
formal statement (Lean)
143theorem gammaMassQCD1L_zero : gammaMassQCD1L 0 = 0 := by
proof body
Term-mode proof.
144 simp [gammaMassQCD1L]
145
146/-! ## RK4 integrator scaffold with enclosure bounds -/
147
148/-- RK4 increment from stage values `(k1,k2,k3,k4)`. -/