pith. sign in
module module high

IndisputableMonolith.Physics.QCDRGE.TwoLoopAlphaS

show as:
view Lean formalization →

TwoLoopAlphaS supplies the two-loop beta coefficients and running formula for the strong coupling α_s. Quark mass scorecard modules cite these definitions when evolving couplings from the M_Z anchor to heavy-quark scales. The module defines N_c, C_F, b0, b1 together with lemmas that verify positivity when the denominator stays positive and reduction to the one-loop case when b1 vanishes.

claim$N_c=3$, $C_F=4/3$, $b_0=(11N_c-2N_f)/(12π)$, $b_1$ the standard two-loop coefficient; the running satisfies the integrated two-loop form $α_s(μ)$ with the stated b0 and b1.

background

AlphaRunning fixes α_s=2/17 at M_Z and gives the one-loop beta function b0=(11N_c-2N_f)/(12π)>0 for N_f<17, establishing asymptotic freedom. StrongForce derives the strong coupling from planar symmetries of the ledger while Constants supplies the base time quantum τ0=1. This module adds the two-loop coefficient b1 and the integrated running function.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

BottomMSBarScoreCard, CharmMSBarScoreCard and TopMSBarScoreCard import these definitions to run masses between the RS anchor and the quark scales. MassAnomalousDimension, PoleToMSbar and ThresholdMatching likewise depend on the two-loop running for consistent NLO evolution across flavor thresholds.

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)