beta0QCDReal
plain-language theorem explainer
beta0QCDReal supplies the real-valued one-loop QCD beta coefficient by casting the rational beta0QCD output. Modelers of alpha_s running in renormalization group flows cite it when assembling the differential equation for the strong coupling. The definition is a direct type coercion that feeds real arithmetic into the one-loop beta function.
Claim. The one-loop QCD beta coefficient is the real number $11 - (2 n_f)/3$.
background
The RGTransport module defines renormalization group transport for mass residues, where the integrated anomalous dimension yields the residue f that relates structural mass at the anchor scale to physical mass via the phi-ladder. The local setting uses lambda = ln phi as normalization and connects running couplings to the mass formula m_phys = m_struct * phi^{-f}. beta0QCDReal rests on beta0QCD, which encodes the rational coefficient in the convention beta0 = 11 - 2 nf / 3, and on the upstream beta0 definition that supplies the related one-loop form (11 Nc - 2 Nf)/(12 pi).
proof idea
One-line wrapper that applies the cast from beta0QCD to the real numbers.
why it matters
beta0QCDReal supplies the real coefficient required by betaQCD1L to realize the one-loop running d alpha_s / d ln mu = -(beta0 / (2 pi)) alpha_s^2. This kernel sits inside the RG transport that defines the empirical mass residue f^exp and links to the phi-ladder mass formula. It closes the interface between the rational beta0QCD and real arithmetic needed for integration against the anomalous dimension in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.