critical_flavor_number
plain-language theorem explainer
The critical flavor number theorem establishes that the one-loop QCD beta coefficient b0 remains positive for 16 quark flavors but becomes non-positive at 17, pinpointing the threshold for asymptotic freedom in QCD. Particle physicists studying running couplings in the Recognition Science framework would cite this result to bound the number of active flavors. The proof proceeds as a direct term-mode verification by unfolding the definition of b0 and applying numerical normalization.
Claim. $b_0(16) > 0$ and $b_0(17) ≤ 0$, where $b_0(n_f) := 11 - (2/3)n_f$ is the one-loop coefficient in the QCD beta function.
background
In the module on Renormalization Group and Running Couplings from RS φ-Ladder, the RS anchor scale μ* = 182.201 GeV serves as a stationarity point of the RG flow. Asymptotic freedom in QCD follows from the SU(3) color structure forced by Q3. The β-function sign is determined by the φ-ladder derivative of the coupling, with the one-loop formula α_s(μ) = α_s(μ*) / (1 + b0/(2π) α_s(μ*) ln(μ/μ*)).
proof idea
The proof is a term-mode proof that applies the constructor tactic to split the conjunction into two goals. For each goal it unfolds the definition of b0_qcd and invokes norm_num to verify the numerical inequality directly.
why it matters
This declaration fills the critical flavor number step in the running couplings analysis, directly supporting the asymptotic freedom criterion for n_f ≤ 16. It connects to the Recognition Science framework where asymptotic freedom in QCD is forced by the SU(3) structure from Q3 and the phi-ladder. The result bounds the flavor count for which the beta function remains negative, consistent with the one-loop running formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.