TwoLoopAlphaSCert
The TwoLoopAlphaSCert structure certifies positivity of the one-loop and two-loop beta-function coefficients b0 and b1 at five active flavors together with exact reduction of the two-loop running formula to the input coupling at the reference scale. QCD modelers in the Recognition Science framework cite this certificate when confirming the two-loop extension of alpha_s running. It is assembled as a record from the positivity lemmas at Nf=5 and the anchor-reduction theorem.
claimThe structure asserts that the beta-function coefficients satisfy $b_0(5)>0$ and $b_1(5)>0$, and that the two-loop running coupling obeys $1/alpha_s(mu)=1/alpha_s(mu_0)+beta_0 log(mu^2/mu_0^2)+(beta_1/beta_0)log(1+beta_0 alpha_s(mu_0)log(mu^2/mu_0^2))$ reduces to the identity $alpha_s(mu_0;alpha_0,N_f,mu_0)=alpha_0$ for all $mu_0>0$.
background
This module derives the closed-form two-loop solution of the QCD renormalization-group equation in the MS-bar scheme. The beta function is d alpha_s / d log mu^2 = -beta0 alpha_s^2 - beta1 alpha_s^3, with beta0=(11 N_c - 2 N_f)/(12 pi) and beta1=(102-38 N_f/3)/(8 pi^2) for SU(3). The integrated expression for the running coupling appears in the module documentation. The certificate packages the sign conditions at the physical flavor number N_f=5 and the normalization at the anchor scale mu=mu_0.
proof idea
As a structure definition the construction simply packages three fields. The positivity fields are supplied by the lemmas b0_at_Nf5_pos and b1_at_Nf5_pos. The reduction field is supplied by the theorem alpha_s_two_loop_at_anchor, which substitutes the scale ratio equal to one into the running formula and simplifies the logarithm to zero.
why it matters in Recognition Science
The certificate is instantiated by the theorem twoLoopAlphaSCert_holds in the same module. It belongs to the Heavy Quark closure track that upgrades the one-loop alpha_s running to two loops, providing the positivity and anchor facts required for later threshold matching. It connects to the Recognition Science constants through the phi-ladder mass formulas but remains within the QCD sector.
scope and limits
- Does not compute numerical values of alpha_s at specific scales.
- Does not incorporate quark-threshold matching.
- Does not prove higher-loop corrections beyond two loops.
- Does not address scheme dependence beyond MS-bar.
formal statement (Lean)
123structure TwoLoopAlphaSCert where
124 /-- One-loop coefficient is positive at N_f = 5. -/
125 b0_at5_pos : 0 < b0 5
126 /-- Two-loop coefficient is positive at N_f = 5. -/
127 b1_at5_pos : 0 < b1 5
128 /-- The running formula reduces to identity at the anchor scale. -/
129 reduces_at_anchor : ∀ (alpha_0 : ℝ) (N_f : ℕ) (mu_0_GeV : ℝ),
130 0 < mu_0_GeV → alpha_s_two_loop alpha_0 N_f mu_0_GeV mu_0_GeV = alpha_0
131