alpha_s_two_loop_b1_zero_eq_one_loop
plain-language theorem explainer
The declaration shows that the two-loop MS-bar running formula for the strong coupling reduces exactly to the one-loop expression when the b1 correction term vanishes. QCD phenomenologists would cite it to confirm perturbative consistency in the limit of negligible higher-order beta-function contributions. The proof is a direct algebraic reduction obtained by unfolding b0 and N_c then normalizing with the ring tactic.
Claim. For real numbers $alpha_0, mu, mu_0$, the two-loop inverse-coupling formula with the $b_1$-induced correction set to zero satisfies $1 + b_0(5) alpha_0 log(mu^2/mu_0^2) = 1 + (11 N_c - 10)/(12 pi) alpha_0 log(mu^2/mu_0^2)$, where $N_c = 3$ and $b_0(5)$ is the leading beta-function coefficient at five active flavors.
background
The module implements the standard two-loop solution of the QCD beta function in the MS-bar scheme. With $N_c$ defined as the number of colors (equal to 3) and $b_0(N_f)$ the leading coefficient $(11 N_c - 2 N_f)/(12 pi)$, the running formula reads $1/alpha_s(mu) = 1/alpha_s(mu_0) + b_0 log(mu^2/mu_0^2) + (b_1/b_0) log(1 + b_0 alpha_0 log(mu^2/mu_0^2))$. The present theorem isolates the reduction obtained by nullifying the $b_1$ term. It extends the one-loop running already present in the imported AlphaRunning module and sits inside the Heavy Quark closure track of the Recognition Science framework.
proof idea
The proof is a one-line wrapper: unfold the definitions of b0 and N_c, then apply the ring tactic to equate the two sides of the real-number identity.
why it matters
The result closes the consistency check between the two-loop and one-loop expressions inside the QCD running module. It supports the module's claim that the two-loop beta function reduces to the simpler case when higher-order corrections are switched off, without threshold matching. No downstream uses are recorded, so the identity functions as an internal sanity check for the perturbative expansion in the Recognition Science treatment of strong-force running.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.