asymptotic_freedom
plain-language theorem explainer
The theorem shows that the one-loop beta coefficient beta0 stays positive at five active quark flavors, the value assigned at the Z scale. QCD phenomenologists would cite it to anchor the sign that produces asymptotic freedom in the running coupling. The proof is a direct term application of the general positivity lemma for beta0 after a norm_num check that the flavor count satisfies the required bound.
Claim. $0 < b_0(5)$ where $b_0(N_f) = (11 N_c - 2 N_f)/(12 π)$ with $N_c = 3$ and $N_f = 5$ the number of active flavors at the Z-boson mass.
background
The module treats the one-loop running of the strong coupling α_s inside Recognition Science. The coefficient b0 is defined as (11 N_c - 2 N_f)/(12 π) with N_c fixed at 3; positivity of b0 for N_f ≤ 16 is the algebraic condition for asymptotic freedom. N_f_Z is the concrete constant 5 used at the Z scale. The upstream lemma beta0_pos states that b0(N_f) > 0 whenever N_f ≤ 16 and supplies the nlinarith argument that converts the integer bound into the real inequality.
proof idea
One-line term proof that applies the upstream lemma beta0_pos to the constant N_f_Z. The hypothesis N_f ≤ 16 is discharged by unfolding the definition of N_f_Z followed by norm_num.
why it matters
This result supplies the concrete positivity instance required by the downstream theorem in QFT.Confinement that states asymptotic freedom at short distance, the Gross-Politzer-Wilczek result. In the RS setting it confirms that the beta function sign remains correct when the flavor count is taken from the Z-scale value, thereby linking the Recognition Composition Law running to the observed weakening of the strong force at high momentum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.