pith. sign in
module module high

IndisputableMonolith.Physics.QCDRGE.PoleToMSbar

show as:
view Lean formalization →

Module supplying the one-loop pole-to-MSbar quark mass conversion coefficient 4/3, universal from C_F. Heavy-quark phenomenologists cite it when mapping PDG pole masses to MSbar values inside the RS framework. Content consists of conversion-factor definitions plus a certification theorem.

claimThe one-loop coefficient in the pole-to-MSbar mass relation is $K_1 = 4/3$, universal and arising from the color factor $C_F$.

background

Module lies in the QCD RGE track and imports the two-loop alpha_s running. Upstream TwoLoopAlphaS extends the one-loop alpha_s_running to include the second beta-function coefficient b1, giving the standard MSbar two-loop running formula. The present module introduces pole_factor, m_pole_from_MS and related conversion functions that implement the one-loop term 4/3.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

Module is imported by TopMSBarScoreCard, which applies the conversion to the top quark (RS rung t=21) with PDG pole mass 172.69 GeV. It supplies the one-loop mass-relation step required for the heavy-quark closure track.

scope and limits

used by (1)

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

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (12)