beta0_SUN
plain-language theorem explainer
beta0_SUN encodes the standard one-loop beta coefficient for SU(N) gauge theories with N_f flavors as the rational (11N - 2N_f)/3. QCD and electroweak modelers cite it to confirm asymptotic freedom when the result is positive. The definition is a direct algebraic expression that downstream theorems instantiate for specific groups and flavor counts.
Claim. The one-loop beta function coefficient for an SU(N) gauge theory with N_f fermion flavors is given by $β_0 = (11N - 2N_f)/3$.
background
The QFT module derives running couplings from φ-ladder scaling, where distinct rungs label energy scales and J-cost optimization changes with rung. The beta coefficient controls the logarithmic derivative of the coupling with respect to scale; positive values produce asymptotic freedom for the strong force. The upstream has class from AsteroidOreSpectroscopy supplies the spectral-peak relation ω_k = ω_0 · φ^k that discretizes the ladder into the same φ-based energy steps used here.
proof idea
One-line definition that directly transcribes the algebraic formula (11N - 2Nf)/3 into Lean rationals. No lemmas or tactics are applied; the expression is the complete body.
why it matters
The definition supplies the numerical input for qcd_asymptotic_free, qcd_beta0_positive, su2_beta0 and the RunningCouplingsProofs structure. It realizes the RS claim that running couplings arise from φ-ladder J-cost variation, linking directly to the T7 eight-tick octave and the D = 3 spatial dimensions of the forcing chain. It closes the interface between standard perturbative QFT and Recognition Science without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.