pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Physics.QCDRGE.AlphaRunning

show as:
view Lean formalization →

AlphaRunning defines the one-loop beta coefficient beta0 and the explicit running formula alpha_s_running for the strong coupling from its value at the Z boson mass. QCD phenomenologists extending one-loop results to two-loop or lattice matching would cite these objects. The module assembles N_c, N_f_Z and the boundary condition alpha_s_MZ into the standard logarithmic running expression without further derivation.

claimThe one-loop coefficient $b_0 = (11/3)N_c - (2/3)N_f$ and the running coupling $a_s(Q) = a_s(M_Z) / (1 + b_0 a_s(M_Z) log(Q^2/M_Z^2)/(4 pi))$, with $N_c=3$, $N_f$ evaluated at the Z scale, and $a_s(M_Z)$ taken from the strong-force boundary condition.

background

The module operates inside the QCD renormalization-group track of Recognition Science. It imports the RS time quantum tau_0 from Constants and the T15 strong-force derivation from StrongForce, which obtains alpha_s(M_Z) from planar edge geometry of the ledger. Sibling definitions introduce N_c, N_f_Z, beta0, alpha_s_MZ and the function alpha_s_running that implements the one-loop flow.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

AlphaRunning supplies the one-loop running that TwoLoopAlphaS imports and extends by adding the second beta coefficient b1 to reach the standard MS-bar two-loop formula. It therefore completes the base layer of the QCD RGE chain that begins from the T15 strong-force hypothesis.

scope and limits

used by (1)

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

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (13)