su2_beta0
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.
claimIn 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 in Recognition Science
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.
scope and limits
- Does not derive the coefficient from the Recognition Composition Law or J-cost functional.
- Does not compute the coupling value at any specific phi-ladder rung or energy scale.
- Does not include two-loop or higher contributions to the beta function.
- Does not address electromagnetic running or the alpha inverse band.
Lean usage
def proofs : RunningCouplingsProofs := { qcd_af := qcd_asymptotic_free, su2_beta := su2_beta0, gut_structure := gut_24_from_8_times_3, proton_ratio := proton_qcd_ratio }formal statement (Lean)
68theorem su2_beta0 : beta0_SUN 2 6 = 10/3 := by native_decide
proof body
Term-mode proof.
69
70/-! ## φ-Ladder Connection -/
71
72/-- Energy scale at φ-ladder rung n, in units of reference scale E₀. -/