alpha_s_two_loop_pos_when_denom_pos
plain-language theorem explainer
The theorem proves that the two-loop MS-bar strong coupling stays positive whenever the reference coupling alpha_0 is positive and the integrated beta-function denominator remains positive. QCD phenomenologists would cite it to confirm that perturbative evolution does not produce unphysical negative values inside the two-loop validity window. The proof is a one-line term that unfolds the closed-form definition of alpha_s_two_loop and applies div_pos to the two input inequalities.
Claim. If $0 < alpha_0$ and $0 < 1 + b_0(N_f) alpha_0 log(mu^2 / mu_0^2) + (b_1(N_f)/b_0(N_f)) alpha_0 log(1 + b_0(N_f) alpha_0 log(mu^2 / mu_0^2))$, then the two-loop running coupling $alpha_s^{(2)}(alpha_0, N_f, mu, mu_0) > 0$.
background
The module solves the two-loop renormalization-group equation for the strong coupling in the MS-bar scheme. With N_c = 3 the beta-function coefficients are b0 = (11 N_c - 2 N_f)/(12 pi) and b1 = (34 N_c^2 - (10 N_c + 6 C_F) N_f)/(24 pi^2). The integrated expression is 1/alpha_s(mu) = 1/alpha_s(mu_0) + b0 log(mu^2/mu_0^2) + (b1/b0) log(1 + b0 alpha_s(mu_0) log(mu^2/mu_0^2)), which rearranges to alpha_s(mu) = alpha_0 divided by the denominator appearing in the hypothesis.
proof idea
The proof unfolds the definition of alpha_s_two_loop and applies div_pos directly to the two positivity hypotheses h_alpha_pos and h_denom_pos. No additional lemmas or tactics are used.
why it matters
The result guarantees that the two-loop formula remains positive inside the perturbative window, supporting the RS anchor value alpha_s(M_Z) = 2/17 that lies inside the PDG bracket. It forms a basic sanity check before threshold matching is introduced in later modules and connects the standard QCD running to the Recognition Science constants track.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.