beta0QCD_nf0
plain-language theorem explainer
The one-loop QCD beta coefficient evaluates to 11 for zero active fermion flavors. Researchers computing mass residues in the Recognition Science framework cite this when initializing the pure-glue running of the strong coupling. The proof is a one-line wrapper that applies norm_num directly to the definition of beta0QCD.
Claim. The one-loop QCD beta coefficient in the convention $beta_0 = 11 - (2/3) n_f$ satisfies $beta_0(0) = 11$.
background
The RGTransport module formalizes renormalization group transport for mass residues. It defines the integrated residue $f$ from the mass anomalous dimension $gamma_m$, normalized by $lambda = ln phi$, and relates the structural mass at the anchor scale to the physical mass via the phi-ladder. The upstream definition states that beta0QCD is the one-loop QCD beta coefficient in the convention beta0 = 11 - 2*nf/3.
proof idea
This is a one-line wrapper that applies the norm_num tactic to the definition of beta0QCD.
why it matters
This supplies the base value for the QCD beta function in the zero-flavor limit, which enters the one-loop running coupling within the RGTransport module. It anchors the leading term in RG transport calculations for structural masses at the phi-ladder anchor, consistent with the mass formula in the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.