TwoLoopAlphaSCert
plain-language theorem explainer
The structure packages three propositions: positivity of the one-loop beta coefficient b0 at five active flavors, positivity of the two-loop coefficient b1 at the same point, and exact reduction of the two-loop MS-bar running formula to the input value at the reference scale. QCD model builders would cite the certificate when confirming consistency of the closed-form alpha_s evolution before adding threshold corrections. The definition is a direct record of three already-proved sibling statements with no additional reasoning steps.
Claim. Let $b_0(N_f)$ and $b_1(N_f)$ be the one- and two-loop coefficients of the QCD beta function in the MS-bar scheme, and let $alpha_s_two_loop(alpha_0, N_f, mu_0, mu)$ be the explicit two-loop solution for the running coupling. The structure asserts $b_0(5) > 0$, $b_1(5) > 0$, and $alpha_s_two_loop(alpha_0, N_f, mu_0, mu_0) = alpha_0$ for every $alpha_0 > 0$ and every $mu_0 > 0$.
background
The module supplies the standard two-loop MS-bar running formula for the strong coupling. The beta function is written $d alpha_s / d log mu^2 = -b0 alpha_s^2 - b1 alpha_s^3 + O(alpha_s^4)$, with the explicit coefficients b0 and b1 given in terms of $N_c = 3$ and the number of active flavors $N_f$. The closed-form solution alpha_s_two_loop is obtained by integrating this equation to two loops without threshold matching. The local setting is the first module of the Heavy Quark closure track, which extends the existing one-loop running from AlphaRunning.
proof idea
The structure is introduced by naming the three fields directly. Each field is filled by an existing sibling proposition: b0_at_Nf5_pos for the first, b1_at_Nf5_pos for the second, and alpha_s_two_loop_at_anchor for the third. No tactics or reductions occur inside the structure itself.
why it matters
The certificate is consumed by the theorem twoLoopAlphaSCert_holds, which assembles an explicit inhabitant. It supplies the basic positivity and anchor-consistency checks required before the next module adds threshold matching. The construction sits inside the two-loop extension of the strong-force sector and ensures the running formula recovers the input coupling at the reference scale, consistent with the overall Recognition Science treatment of constants in the strong sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.