no_asymptotic_freedom_17
plain-language theorem explainer
The theorem shows that the one-loop QCD beta coefficient b0 equals -1/3 at 17 active quark flavors and is therefore non-positive. High-energy physicists modeling flavor extensions or grand-unified scenarios would cite the bound to exclude n_f >=17 while preserving asymptotic freedom. The proof is a one-line wrapper that unfolds the explicit definition of b0_qcd and reduces the arithmetic by norm_num.
Claim. $b_0(17) = 11 - 2*17/3 = -1/3$ and therefore $b_0(17) <= 0$, where $b_0(n_f) = 11 - (2/3)n_f$ is the one-loop coefficient of the QCD beta function.
background
The module derives the renormalization-group beta function from the phi-ladder derivative of the coupling, with the sign fixed by the SU(3) color structure that follows from the Q3 forcing step. The definition b0_qcd(n_f) := 11 - 2*n_f/3 is introduced directly; asymptotic freedom requires b0 >0 and therefore n_f <16.5. The upstream structure 'for' supplies the meta-realization axioms that embed the self-reference content into the forcing chain T0-T8.
proof idea
The term proof unfolds the definition b0_qcd and hands the resulting arithmetic expression to norm_num, which evaluates 11 - 34/3 to -1/3 and confirms the inequality.
why it matters
The result closes the upper edge of the asymptotic-freedom window stated in the module (n_f <=16) and supplies the concrete bound needed for the sibling critical_flavor_number theorem. It inherits the beta-function structure beta(g) = (1/ln phi) dg/dr from the phi-ladder derivative and the T5 J-uniqueness that forces the standard one-loop coefficient form.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.