su2_beta0
plain-language theorem explainer
The declaration shows that the leading beta-function coefficient for SU(2) gauge theory with six fermion flavors equals 10/3. Researchers assembling running-coupling summaries in the Recognition Science QFT setting would cite this when confirming positive coefficients for asymptotic freedom. The proof is a one-line wrapper that applies a native decision procedure to the algebraic expression.
Claim. In SU(2) Yang-Mills theory coupled to six Dirac fermions, the one-loop beta-function coefficient satisfies $beta_0 = 10/3$.
background
The module derives running couplings from phi-ladder scaling, where each rung corresponds to a discrete energy level and J-cost optimization varies across tiers. Different rungs produce the observed scale dependence of alpha, alpha_s, and alpha_W via the renormalization group flow expressed in RS-native units. Upstream results supply rung calibrations from nuclear densities and ore classes, energy as a real number, and scale as phi to the power k, which anchor the discrete energy tiers used in the beta coefficient.
proof idea
The proof is a one-line wrapper that invokes native_decide to evaluate the beta coefficient expression for SU(2) with six flavors and confirm the exact rational value 10/3.
why it matters
This result supplies the su2_beta entry in the runningCouplingsProofs structure that aggregates QCD asymptotic freedom, GUT structure, and proton ratio. It advances the module target of obtaining running couplings from phi-scaling and connects to the forcing chain landmarks of J-uniqueness and the eight-tick octave. It closes a computational verification step for positive beta_0 without touching open questions on higher-order terms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.