beta0QCD
plain-language theorem explainer
The definition supplies the standard one-loop beta coefficient for QCD as beta0(nf) = 11 - (2/3)nf in rationals. Particle physicists modeling renormalization group flows and mass residues in the Recognition Science framework cite it when deriving running couplings or asymptotic freedom bounds. It is introduced as a direct algebraic expression with no lemmas or tactics applied.
Claim. The one-loop QCD beta coefficient is defined by $beta_0(n_f) = 11 - (2/3) n_f$, where $n_f$ is the number of active fermion flavors.
background
The RGTransport module formalizes renormalization group transport that defines the empirical mass residue f^exp. Fermion masses run with scale according to d(ln m)/d(ln mu) = -gamma_m(mu), and the integrated residue f(mu0, mu1) = (1/lambda) integral gamma_m d(ln mu) enters the structural mass formula m_phys = m_struct * phi^{-f} with lambda = ln phi. Upstream structures supply the J-cost minimization (strictly convex at x=1), the spectral emergence of SU(3)xSU(2)xU(1) gauge content with exactly three generations, and phi-forcing derived relations that calibrate the overall framework.
proof idea
The declaration is a direct definition that subtracts (2/3)nf from the rational constant 11. No lemmas are applied and no tactics are invoked; it serves as the base expression unfolded by downstream results such as beta0QCD_nf0 and beta0QCD_asymp_free.
why it matters
This definition anchors the one-loop QCD running inside the RGTransport module and feeds the real-valued view beta0QCDReal together with the asymptotic-freedom theorem for nf <= 16. It supports the integrated anomalous-dimension residue that converts structural masses on the phi-ladder into physical masses, consistent with the T5 J-uniqueness and T7 eight-tick octave from the forcing chain. No open scaffolding questions are attached.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.