beta0QCD_asymp_free
plain-language theorem explainer
The one-loop QCD beta coefficient remains strictly positive for any natural number of quark flavors up to 16, confirming the ultraviolet asymptotic freedom of the strong coupling. Researchers modeling renormalization group evolution of α_s cite this bound when validating perturbative QCD for the Standard Model's six flavors. The tactic proof unfolds the explicit formula 11 - (2 nf)/3 and chains rational inequalities to show the subtracted term stays below 11.
Claim. For every natural number $n_f$ satisfying $n_f ≤ 16$, the one-loop QCD beta coefficient obeys $β_0(n_f) = 11 - (2/3) n_f > 0$.
background
In the RG transport module the one-loop QCD beta coefficient is introduced by the definition beta0QCD(nf) := 11 - (2 nf)/3, where nf counts active quark flavors. This coefficient multiplies the leading term in the beta function that governs the scale dependence of the strong coupling, and it enters the integrated residue f that relates structural masses at the anchor scale to physical masses via the phi-ladder. The upstream result beta0QCD supplies the explicit rational expression; the module context links such coefficients to the anomalous-dimension integrals that define the empirical mass residue f^exp between renormalization points.
proof idea
The proof unfolds beta0QCD to expose the expression 11 - (2 nf)/3. It casts the hypothesis nf ≤ 16 into rationals via exact_mod_cast, applies div_le_div_of_nonneg_right together with nlinarith to obtain (2 nf)/3 ≤ (2·16)/3, uses norm_num to verify 32/3 < 11, combines the bounds with lt_of_le_of_lt, and finishes with linarith to conclude positivity.
why it matters
This algebraic positivity check underpins the validity of one-loop RG transport for the strong sector when nf ≤ 16, directly supporting the beta0QCD definition in the same module and the broader framework of running couplings that feed into mass-residue calculations. It aligns with the Recognition Science treatment of renormalization-group flows that connect structural masses to observed residues, though no downstream theorems yet depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.