pith. sign in
module module high

IndisputableMonolith.Physics.QCDRGE.TwoLoopAlphaS

show as:
view Lean formalization →

The TwoLoopAlphaS module supplies the two-loop beta coefficients and integrated running formula for the strong coupling α_s, extending the one-loop result from AlphaRunning. It defines N_c, C_F, b0, b1 and proves reduction to one-loop when b1 vanishes plus positivity of the running expression. Quark mass scorecards and threshold routines cite these lemmas to convert RS anchor values to PDG scales. The module consists of constant declarations followed by algebraic lemmas.

claim$N_c = 3$, $C_F = 4/3$, $b_0 = (11N_c - 2N_f)/(12π)$, $b_1$ the two-loop coefficient, and the two-loop running function α_s(μ) obtained by integrating the beta equation with initial value α_s(M_Z) = 2/17.

background

The module sits inside the QCD renormalization group section and imports the base RS time quantum from Constants, the one-loop running from AlphaRunning, and the strong-force derivation from StrongForce. AlphaRunning states that b0 = (11N_c - 2N_f)/(12π) > 0 for N_f < 17, ensuring asymptotic freedom, while StrongForce sets the anchor value α_s(M_Z) = 2/17 from ledger geometry. Definitions introduced here are the number of colors N_c, the fundamental Casimir C_F, the one-loop coefficient b0, and the two-loop coefficient b1 together with the integrated running expression.

proof idea

Constants N_c, C_F, b0, b1_pos_lowNf and b1_at_Nf5_pos are declared first. The function alpha_s_two_loop is defined by the closed-form two-loop integral. The lemma alpha_s_two_loop_b1_zero_eq_one_loop is proved by direct substitution showing exact reduction when b1 vanishes. Positivity lemmas check the sign of the denominator for N_f in the physical range. All steps use algebraic simplification and case splits on N_f.

why it matters in Recognition Science

This module feeds the two-loop corrections required by BottomMSBarScoreCard, CharmMSBarScoreCard, TopMSBarScoreCard, MassAnomalousDimension, PoleToMSbar and ThresholdMatching. It extends the one-loop approximation of AlphaRunning to the precision needed for RS mass predictions against PDG MS-bar values. The b1 terms close the accuracy gap for running between the M_Z anchor and the charm or bottom scales.

scope and limits

used by (6)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (13)