beta0_SUN
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the coefficient from the Recognition Composition Law or J-cost equation.
- Does not include two-loop or higher corrections to the beta function.
- Does not map φ-rung indices to explicit energy values in GeV.
- Does not treat non-perturbative or lattice effects.
Lean usage
theorem qcd_beta0_positive : beta0_SUN 3 6 = 7 := by native_decideformal statement (Lean)
58def beta0_SUN (N Nf : ℕ) : ℚ := (11 * N - 2 * Nf) / 3
proof body
Definition body.
59
60/-- **THEOREM**: QCD (SU(3)) with 6 flavors has β₀ = 7 > 0. -/