pith. machine review for the scientific record. sign in
theorem proved term proof high

twoLoopAlphaSCert_holds

show as:
view Lean formalization →

The theorem certifies that the two-loop MS-bar running formula for the strong coupling satisfies positivity of both beta-function coefficients at five active flavors together with exact reduction to the input value at the reference scale. QCD model builders and lattice groups working inside the Recognition Science mass-ladder construction would cite the result when validating their alpha_s evolution against the closed-form expression. The proof is a direct term-mode construction that assembles the certificate structure from three separate lemma

claimLet $b_0(N_f)$ and $b_1(N_f)$ denote the one- and two-loop beta-function coefficients in the MS-bar scheme for $N_c=3$. Then $b_0(5)>0$, $b_1(5)>0$, and the two-loop running satisfies $1/alpha_s(mu)=1/alpha_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))$ with equality to the input coupling whenever $mu=mu_0>0$.

background

The module supplies the closed-form two-loop solution of the QCD beta function in the MS-bar scheme, extending the existing one-loop running. The beta function reads d alpha_s / d log mu^2 = -beta0 alpha_s^2 - beta1 alpha_s^3 + O(alpha_s^4), with beta0 = b0(N_f) = (11 N_c - 2 N_f)/(12 pi) and beta1 = b1(N_f) = (102 - 38 N_f/3)/(8 pi^2). The structure TwoLoopAlphaSCert packages the three properties required for downstream heavy-quark modules: positivity of b0 at N_f=5, positivity of b1 at N_f=5, and exact anchoring at the reference scale.

proof idea

The proof is a term-mode construction that directly supplies the three fields of TwoLoopAlphaSCert. It assigns b0_at5_pos to the lemma b0_at_Nf5_pos, b1_at5_pos to b1_at_Nf5_pos, and reduces_at_anchor to the lemma alpha_s_two_loop_at_anchor. No additional tactics or reductions are performed.

why it matters in Recognition Science

This declaration certifies the two-loop running formula as Module 1 of the Heavy Quark closure track. It supplies the positivity and anchoring properties needed to extend the one-loop AlphaRunning module into the Recognition Science mass-ladder calculations. The result anchors the strong-coupling evolution used in phi-ladder mass formulas and connects directly to the asymptotic-freedom requirement encoded in b0>0.

scope and limits

formal statement (Lean)

 132theorem twoLoopAlphaSCert_holds : TwoLoopAlphaSCert :=

proof body

Term-mode proof.

 133  { b0_at5_pos := b0_at_Nf5_pos
 134    b1_at5_pos := b1_at_Nf5_pos
 135    reduces_at_anchor := alpha_s_two_loop_at_anchor }
 136
 137end
 138
 139end IndisputableMonolith.Physics.QCDRGE.TwoLoopAlphaS

depends on (4)

Lean names referenced from this declaration's body.