qcd_beta_nf17
plain-language theorem explainer
The declaration establishes that the one-loop QCD beta-function coefficient for three colors and seventeen flavors equals exactly negative one third. QCD phenomenologists analyzing the boundary of asymptotic freedom and the onset of the conformal anomaly would cite this when locating the critical flavor number. The proof is a direct arithmetic evaluation of the closed-form coefficient expression via native decision procedures.
Claim. The one-loop beta-function coefficient for QCD with $N_c=3$ colors and $N_f=17$ flavors satisfies $(11N_c-2N_f)/3=-1/3$.
background
In the QFT anomalies module the coefficient is introduced via the definition qcdBetaCoeff(Nc,Nf):=(11Nc-2Nf)/3, which controls the one-loop running of the strong coupling and the associated conformal anomaly. The module frames anomalies as consequences of 8-tick phase mismatches that break classical scale invariance. The unrelated beta symbols appearing in the PPN and partition-function modules denote the post-Newtonian parameter and inverse temperature, respectively.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to evaluate the arithmetic expression (113-217)/3 directly.
why it matters
This supplies the explicit negative value required by the downstream theorem qcd_no_af_nf17, which concludes that seventeen flavors render QCD non-asymptotically free. It completes the concrete step in the module's treatment of conformal anomalies arising from 8-tick phase mismatches, where the sign change in the beta coefficient marks loss of scale invariance. The result places the critical flavor count between sixteen and seventeen, consistent with the framework's eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.