b0_at_Nf5_pos
b0(5) > 0 holds for the one-loop beta coefficient in five-flavor QCD, securing the negative sign of the beta function and thus asymptotic freedom. QCD running analyses cite this when fixing the number of active flavors at the Z-pole. The term proof unfolds b0 and N_c then reduces via div_pos and norm_num.
claim$0 < b_0(5)$ where $b_0(N_f) := (11 N_c - 2 N_f)/(12 pi)$ and $N_c = 3$.
background
The Two-Loop QCD Running module extends one-loop alpha_s running by including the second beta-function coefficient b1 in the MS-bar scheme. The beta function is d alpha_s / d log mu^2 = -beta0 alpha_s^2 - beta1 alpha_s^3 + O(alpha_s^4), with beta0 = (11 N_c - 2 N_f)/(12 pi) for N_c = 3 colors. The upstream definition of b0 re-exports this canonical form directly from the AlphaRunning module.
proof idea
Unfolds b0 and N_c to obtain the explicit expression (33 - 10)/(12 pi). Applies the div_pos lemma to the positive denominator 12 pi (via the positivity tactic) and uses norm_num to confirm the numerator 23 is positive.
why it matters in Recognition Science
Supplies the b0_at5_pos field inside TwoLoopAlphaSCert_holds that certifies the full two-loop running formula. It also feeds b0_pos_at5 in the MassAnomalousDimension module for the two-loop mass running ratio. This anchors asymptotic freedom at N_f = 5 in the Heavy Quark closure track, consistent with the beta-function sign required by the Recognition Science physics derivations.
scope and limits
- Does not prove b0 positivity at other values of N_f.
- Does not incorporate the two-loop coefficient b1.
- Does not address quark threshold matching or flavor changes.
- Does not derive alpha_s from Recognition Science constants or the phi ladder.
formal statement (Lean)
64theorem b0_at_Nf5_pos : 0 < b0 5 := by
proof body
Term-mode proof.
65 unfold b0 N_c
66 apply div_pos _ (by positivity : (0 : ℝ) < 12 * Real.pi)
67 norm_num
68
69/-- The two-loop running closed form. -/