betaQCD1L_vanishes_at_zero
plain-language theorem explainer
The one-loop QCD beta function vanishes at zero strong coupling for arbitrary flavor count. Modelers of renormalization group flows in QCD cite this to fix the origin as a fixed point before integrating the running. The proof is a one-line simplification that substitutes the explicit quadratic definition of the beta function.
Claim. For any natural number $n_f$, the one-loop QCD beta function satisfies $d alpha_s / d ln mu = -(beta_0(n_f)/(2 pi)) alpha_s^2$ and therefore evaluates to zero when the coupling $alpha_s = 0$.
background
This theorem belongs to the renormalization group transport module, which encodes the integrated mass residue $f(mu_0, mu_1) = (1/lambda) int gamma_m(mu') d ln mu'$ that converts structural masses at the phi-anchor into physical masses via $m_phys = m_struct * phi^{-f}$. The module supplies the mathematical skeleton into which explicit QCD kernels are later inserted, with lambda = ln phi as the fixed normalization scale drawn from the Recognition Science phi-ladder.
proof idea
The proof is a one-line wrapper that applies the simp tactic to the definition of betaQCD1L, which is proportional to alphaS squared and therefore returns zero at the origin.
why it matters
The result supplies the required boundary condition at vanishing coupling for the one-loop running inside the RG transport framework. It confirms that the origin remains a fixed point before any integration of the anomalous dimension that feeds the mass formula. No downstream uses are recorded yet, but the vanishing is a prerequisite for any later connection theorems that relate transport integrals to phi-powered mass ratios.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.