qcd_beta0_positive
plain-language theorem explainer
The declaration establishes that the one-loop beta coefficient for SU(3) with six quark flavors equals seven. Particle physicists confirming the sign of the QCD beta function would cite this when proving asymptotic freedom. The proof reduces to a single native_decide evaluation of the arithmetic formula for the coefficient.
Claim. The one-loop beta function coefficient for SU(3) gauge theory with six quark flavors satisfies $beta_0 = 7$.
background
The module derives running couplings from phi-ladder scaling, where distinct rungs label energy scales and J-cost optimization changes with rung. The coefficient is given explicitly by the definition beta0_SUN(N, Nf) = (11N - 2Nf)/3. This sits inside the Recognition Science treatment of QFT parameters obtained from the forcing chain T0-T8 and the Recognition Composition Law.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the defining arithmetic expression of beta0_SUN at N=3 and Nf=6.
why it matters
This supplies the exact numerical value required by the downstream theorem qcd_asymptotic_free, which rewrites the inequality beta0_SUN 3 6 > 0 and finishes by norm_num. It anchors the standard QCD beta function inside the RS account of scale-dependent J-cost on the phi ladder, consistent with the eight-tick octave and D=3. No open scaffolding is touched.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.