qcd_asymptotic_free
plain-language theorem explainer
The one-loop beta coefficient for SU(3) with six flavors is positive, establishing asymptotic freedom for QCD inside the Recognition Science account of running couplings. A physicist modeling high-energy strong interactions or unification scenarios would cite the result. The proof substitutes the explicit beta formula and reduces the inequality to a direct numerical check.
Claim. For the SU(3) gauge theory with six quark flavors the coefficient satisfies $7 > 0$, where the one-loop beta function is given by $β_0 = (11N - 2N_f)/3$.
background
The module derives running couplings from φ-ladder scaling: different rungs label distinct energy scales and J-cost optimization produces the observed energy dependence of α, α_s and α_W. The auxiliary definition beta0_SUN supplies the standard one-loop coefficient β₀ = (11N − 2N_f)/3 for an SU(N) theory with N_f flavors. The upstream theorem qcd_beta0_positive records the concrete evaluation β₀(SU(3), N_f=6) = 7.
proof idea
The proof is a one-line wrapper that rewrites the goal with qcd_beta0_positive (which replaces beta0_SUN 3 6 by the numeral 7) and then invokes norm_num to discharge the arithmetic inequality 7 > 0.
why it matters
The theorem populates the qcd_af slot inside the runningCouplingsProofs record that assembles all running-coupling results. It thereby completes the QFT-011 derivation of asymptotic freedom from φ-ladder scaling, where positive β₀ corresponds to the strong coupling decreasing toward higher rungs. No open scaffolding remains for this particular claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.