m_pole_from_MS
plain-language theorem explainer
The definition converts an MS-bar quark mass at its own scale to the corresponding pole mass by direct multiplication with the two-loop factor. High-energy physicists aligning Recognition Science mass predictions against PDG pole-mass reports for the top quark would cite this conversion. It is realized as a one-line multiplication that delegates the perturbative coefficients to the sibling definition pole_factor.
Claim. The pole mass is obtained from the MS-bar mass by the relation $m_{pole} = m_{MS} (1 + (4/3) (α_s/π) + K_2(N_l) (α_s/π)^2)$, where $K_2$ is the two-loop coefficient depending on the number of light flavors $N_l$.
background
This module supplies the two-loop conversion between pole and MS-bar masses required to compare Recognition Science predictions with experimental quark-mass reports. The MODULE_DOC states the explicit relation $m_{pole} = m_{MS}(m_{MS}) (1 + (4/3)(α_s/π) + K_2 (α_s/π)^2 + O(α_s^3))$ with $K_2 ≈ 11.1 - 1.04 N_l$. The upstream definition pole_factor supplies the concrete factor $1 + K_1 (α_s/π) + K_2(N_l) (α_s/π)^2$ with $K_1 = 4/3$.
proof idea
The definition is a one-line wrapper that multiplies the input MS-bar mass by the value returned by pole_factor alpha_s N_l.
why it matters
This definition supplies the forward map used by m_pole_from_MS_pos_top to prove positivity and by PoleToMSbarCert to certify two-loop accuracy. It is invoked inside m_t_pole_predicted to produce the predicted pole mass for the top quark from the RS MS-bar reference at the top scale with $N_l = 5$. It thereby connects the Recognition Science mass ladder to the PDG pole-mass observable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.