qcdBetaCoeff
plain-language theorem explainer
The declaration defines the one-loop QCD beta function coefficient as (11 Nc - 2 Nf)/3. Particle physicists checking asymptotic freedom for Nc=3 and varying Nf would cite this when evaluating the sign of the running coupling. It is implemented as a direct algebraic definition with no computation steps.
Claim. The one-loop beta function coefficient for QCD is given by $b = (11 N_c - 2 N_f)/3$.
background
The QFT.Anomalies module derives quantum anomalies from 8-tick phase mismatches, where discrete time structure breaks classical scale invariance and produces the conformal anomaly via running couplings. The beta coefficient controls whether the gauge coupling grows or shrinks with energy scale. Upstream results supply unrelated beta definitions (inverse temperature in partition functions and a PPN parameter), but the present definition stands alone as the standard one-loop QCD expression.
proof idea
Direct definition implementing the standard one-loop QCD beta coefficient formula.
why it matters
This definition is referenced by AnomalyProofSummary and by the theorems qcd_asymptotic_freedom_nf6, qcd_beta_nf6, qcd_critical_flavors, and qcd_no_af_nf17, which locate the loss of asymptotic freedom between 16 and 17 flavors. It supplies the concrete coefficient needed to connect the 8-tick phase structure (T7) to the conformal anomaly in the Recognition Science account of QCD.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.