qcd_asymptotic_freedom_nf6
plain-language theorem explainer
The theorem establishes that the one-loop QCD beta coefficient for three colors and six flavors is positive, confirming asymptotic freedom. Physicists modeling running couplings through discrete phase structures would cite it to link 8-tick mismatches to the conformal anomaly. The proof is a one-line wrapper that substitutes the explicit coefficient value of 7 and checks the inequality numerically.
Claim. For QCD with $N_c=3$ colors and $N_f=6$ flavors the one-loop beta function coefficient satisfies $(11N_c-2N_f)/3>0$.
background
The module derives quantum anomalies from 8-tick phase mismatches between discrete and continuous symmetries. The conformal anomaly appears as broken scale invariance, expressed through the sign of the running-coupling beta coefficient. The coefficient is defined by qcdBetaCoeff Nc Nf := (11Nc-2Nf)/3. Upstream, qcd_beta_nf6 proves that this expression equals 7 when Nc=3 and Nf=6.
proof idea
The proof applies the equality qcd_beta_nf6 to replace the coefficient by 7, then invokes norm_num to confirm 7>0.
why it matters
It supplies the qcd_af field inside the anomalyProofs summary that aggregates all anomaly results. The module doc ties the sign of this coefficient to the conformal anomaly arising from 8-tick discreteness. Within the Recognition framework the positive value is consistent with the T7 eight-tick octave and the alpha band, yet the direct derivation of the beta formula from the J-cost or phi-ladder remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.