pith. sign in
module module high

IndisputableMonolith.Physics.QCDRGE.PoleToMSbar

show as:
view Lean formalization →

The module encodes the universal one-loop pole-to-MS-bar quark mass conversion coefficient of 4/3 arising from C_F in QCD. Top-quark mass scorecards cite these definitions to translate experimental pole masses into MS-bar values aligned with the phi-ladder. It consists of direct definitions for the conversion functions together with a certification that the coefficient is correctly realized.

claimThe one-loop pole-to-MS-bar mass coefficient satisfies $K_1 = 4/3$, entering the leading-order relation $m_ {pole} = m_{MS} (1 + (4/3) (alpha_s / pi) + O(alpha_s^2))$.

background

This module operates inside the QCD renormalization group track for heavy quarks. It imports the two-loop running of alpha_s from TwoLoopAlphaS, whose doc-comment notes that the module extends the one-loop alpha_s_running to include the second beta-function coefficient b_1. Local definitions introduce K_1 as the color-factor coefficient 4/3, pole_factor as the multiplicative correction, and m_pole_from_MS as the explicit conversion map from MS-bar to pole mass.

proof idea

This is a definition module, no proofs. The coefficient is stated directly as 4/3, with auxiliary functions for positive top-quark cases and an invariance check at zero. Certification theorems verify the implementation by direct substitution.

why it matters in Recognition Science

The module feeds the TopMSBarScoreCard, which compares the PDG 2024 top pole mass of 172.69 GeV to the RS prediction at rung t=21. It supplies the translation between pole and MS-bar schemes required to align experimental data with the Recognition Science mass formula on the phi-ladder.

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)