pole_factor
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.