m_MS_from_pole
plain-language theorem explainer
The definition converts a quark pole mass to the equivalent MS-bar mass by multiplying by the inverse of the two-loop QCD pole factor. Particle physicists aligning Recognition Science mass predictions with PDG reports for top, charm, and bottom quarks would cite this conversion. It is realized as a direct multiplication by the pre-defined inverse factor that matches the algebraic inverse of the two-loop expansion.
Claim. The MS-bar mass satisfies $m_{MS} = m_{pole} / f$, where the two-loop pole factor is $f = 1 + (4/3) (α_s / π) + K_2 (α_s / π)^2$ with $K_2 ≈ 11.1 - 1.04 N_l$ and $N_l$ the number of light flavors.
background
The module supplies the pole-to-MS-bar conversion to two-loop accuracy in the MS-bar scheme with $C_F = 4/3$. The defining relation is $m_{pole} = m_{MS}(m_{MS}) (1 + (4/3)(α_s/π) + K_2 (α_s/π)^2 + O(α_s^3))$, where $K_2$ depends on the number of light flavors $N_l$. For the top quark one takes $N_l = 5$, yielding $K_2 ≈ 5.9$. Upstream results include the ledger factorization structure that calibrates the J-cost and the phi-forcing derived structure that supplies the underlying cost function.
proof idea
The definition is a one-line wrapper that multiplies the supplied pole mass by the inverse pole factor evaluated at the given strong coupling and flavor count.
why it matters
This definition supplies the missing inverse direction needed to place all quark masses on a common MS-bar footing for comparison with Recognition Science predictions. It directly supports the two-loop QCD running required by the module and aligns with the phi-ladder mass formula in the broader framework. No parent theorems are registered yet, leaving open its insertion into full RGE chains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.