alpha_s_two_loop
plain-language theorem explainer
This definition supplies the explicit closed-form expression for two-loop running of the strong coupling α_s(μ) in the MS-bar scheme. QCD phenomenologists evolving couplings across scales or building heavy-quark models cite it as the direct extension of the one-loop formula. The body is a pure let-expression that assembles the denominator from the precomputed beta coefficients b0 and b1.
Claim. $α_s(μ) = α_0 / [1 + b_0(N_f) α_0 log(μ²/μ_0²) + (b_1(N_f)/b_0(N_f)) α_0 log(1 + b_0(N_f) α_0 log(μ²/μ_0²))]$, where b_0(N_f) = (11 N_c − 2 N_f)/(12 π) and b_1(N_f) = (102 − 38 N_f/3)/(8 π²) with N_c = 3.
background
Module TwoLoopAlphaS forms the first part of the Heavy Quark closure track and extends the existing one-loop running formula by adding the second beta-function coefficient. The two-loop beta equation is dα_s/d log μ² = −b_0 α_s² − b_1 α_s³ + O(α_s⁴), solved by direct integration to the displayed closed form (no threshold matching is performed here). b_0(N_f) and b_1(N_f) are the canonical SU(3) coefficients supplied by sibling definitions in the same module; upstream integer and rational constructions from IntegersFromLogic and RationalsFromLogic are used only to build the numeric constants inside those coefficients.
proof idea
The declaration is a pure definition that first binds L to the scale logarithm log(μ_GeV²/μ_0_GeV²), then constructs the denominator as 1 + b0 N_f α_0 L + (b1 N_f / b0 N_f) α_0 log(1 + b0 N_f α_0 L), and finally returns α_0 divided by that quantity. No lemmas or tactics are invoked; the expression is the literal transcription of the integrated two-loop solution.
why it matters
The definition is the central object invoked by the anchor identity alpha_s_two_loop_at_anchor, the positivity statement alpha_s_two_loop_pos_when_denom_pos, and the certification structure TwoLoopAlphaSCert. It supplies the two-loop extension required by the Heavy Quark closure track, linking the strong-force sector to the Recognition Science phi-ladder mass formulas and the overall forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.