asymptotic_freedom_criterion
plain-language theorem explainer
In the Recognition Science treatment of QCD running couplings, the one-loop beta coefficient b0 is positive for up to 16 quark flavors, establishing asymptotic freedom. Particle physicists modeling strong interaction renormalization group flow would cite this result when deriving the evolution of the strong coupling or quark masses. The proof is a direct algebraic verification that unfolds the explicit formula for b0 and applies linear arithmetic to the bound n_f ≤ 16.
Claim. For any natural number $n_f$ satisfying $n_f ≤ 16$, the one-loop QCD beta-function coefficient satisfies $b_0(n_f) = 11 - (2/3)n_f > 0$.
background
The module derives renormalization group equations from the Recognition Science phi-ladder. The beta function is obtained as the ladder derivative of the coupling: β(g) = (1/ln φ) dg/dr. The coefficient b0 is defined explicitly as 11 - 2 n_f /3, which fixes the sign of the beta function for SU(3) QCD. The upstream definition states that asymptotic freedom requires b0 >0, i.e., n_f <16.5, and notes that the SM case n_f=6 yields b0=7>0.
proof idea
The proof unfolds the definition of the beta coefficient, casts the natural-number inequality n_f ≤16 to the reals via exact_mod_cast, and closes with linarith.
why it matters
This result is invoked directly in the proof that the mass evolution exponent remains positive for n_f ≤16. It supplies the asymptotic freedom step required by the RS renormalization paper, where the beta sign follows from the phi-ladder derivative and the forced SU(3) color structure. The declaration anchors the perturbative running of alpha_s inside the framework's eight-tick octave and D=3 spatial setting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.