pole_factor
The pole_factor definition supplies the two-loop multiplicative correction converting an MS-bar quark mass at its own scale into the pole mass. QCD phenomenologists aligning RS phi-ladder predictions with PDG top, bottom, and charm values cite it for scheme translation. It is a direct algebraic substitution of the fixed one-loop coefficient 4/3 together with the flavor-dependent two-loop coefficient into the perturbative series.
claimThe two-loop conversion factor from MS-bar mass to pole mass is given by $1 + (4/3) (alpha_s / pi) + (11.1 - 1.04 N_l) (alpha_s / pi)^2$.
background
In the Recognition Science treatment of QCD, the PDG pole mass for the top quark must be converted to the MS-bar scheme used for lighter quarks so that all masses can be compared uniformly against the phi-ladder formula. The module implements the two-loop truncation of the standard perturbative relation m_pole = m_MS (1 + (4/3)(alpha_s/pi) + K_2 (alpha_s/pi)^2 + O(alpha_s^3)), where the one-loop coefficient is fixed at 4/3 from the color factor C_F and the two-loop coefficient is the linear function 11.1 - 1.04 N_l of the number of active light flavors. Upstream, the scale function from LargeScaleStructureFromRS supplies the phi-powered renormalization points at which these masses are evaluated.
proof idea
The definition is a direct algebraic expansion that inserts the precomputed one-loop coefficient 4/3 and the two-loop coefficient 11.1 - 1.04 N_l into the series 1 + (4/3)(alpha_s/pi) + K_2(N_l)(alpha_s/pi)^2. No lemmas or tactics are invoked beyond substitution of the sibling definitions K_1 and K_2.
why it matters in Recognition Science
This definition is the central object used by m_pole_from_MS and m_MS_from_pole to translate between mass schemes and is certified inside the PoleToMSbarCert structure that records the positivity and normalization properties required for RS mass predictions. It implements the two-loop truncation of the QCD pole-MS relation quoted in the module documentation, thereby closing the interface between the Recognition Science phi-ladder masses and experimental quark-mass inputs. The construction sits downstream of the K_1 and K_2 coefficients and feeds the positivity theorem pole_factor_pos_top.
scope and limits
- Does not incorporate three-loop or higher corrections to the conversion.
- Does not enforce any bound on alpha_s or N_l.
- Does not prove that the factor remains positive for given alpha_s.
- Does not connect to the J-function, forcing chain, or Recognition Composition Law.
Lean usage
m_pole_from_MS m_MS alpha_s N_lformal statement (Lean)
40def pole_factor (alpha_s : ℝ) (N_l : ℕ) : ℝ :=
proof body
Definition body.
41 1 + K_1 * (alpha_s / Real.pi) + K_2 N_l * (alpha_s / Real.pi) ^ 2
42
43/-- Convert MS-bar mass at its own scale to pole mass. -/