pith. sign in
module module high

IndisputableMonolith.Physics.QCDRGE.TwoLoopAlphaS

show as:
view Lean formalization →

The module supplies the two-loop beta-function coefficients and explicit running formula for the strong coupling in the Recognition Science setting. Quark-mass scorecards and threshold-matching code cite it to evolve alpha_s between the M_Z anchor and the MS-bar scales of charm, bottom, and top. The module consists of definitions for N_c, C_F, b0, b1 plus supporting positivity and equality lemmas, all machine-checked with zero sorrys.

claim$N_c=3$, $C_F=4/3$, $b_0=(11N_c-2N_f)/(12π)$, $b_1$ the two-loop coefficient, and the explicit two-loop solution for the running coupling $α_s(μ)$ starting from the one-loop anchor $α_s(M_Z)=2/17$.

background

The module belongs to the QCD renormalization-group section and imports the one-loop running from AlphaRunning, which records $α_s=2/17$ at $M_Z$ together with the one-loop coefficient $b_0=(11N_c-2N_f)/(12π)>0$ for $N_f<17$. StrongForce supplies the derivation of that anchor value from planar ledger symmetries, while Constants fixes the base time quantum $τ_0=1$ tick. The sibling definitions introduce the color factors $N_c$ and $C_F$, the two-loop coefficients $b_0$ and $b_1$, and the closed-form two-loop expression for $α_s(μ)$.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module feeds BottomMSBarScoreCard, CharmMSBarScoreCard, TopMSBarScoreCard, MassAnomalousDimension, PoleToMSbar, and ThresholdMatching. It supplies the two-loop running required to compare RS mass predictions at the $M_Z$ anchor with experimental MS-bar values at the individual quark scales. It extends the one-loop AlphaRunning result to the precision needed for the scorecard comparisons.

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)