m_pole_from_MS_pos_top
plain-language theorem explainer
Positivity of the top-quark pole mass follows from a positive MS-bar mass and a strong coupling strictly between zero and one half. QCD phenomenologists converting between pole and MS-bar schemes cite this result when verifying that RS-derived masses remain positive. The proof is a one-line term wrapper that unfolds the conversion definition and applies multiplication positivity to the MS-bar mass hypothesis together with the already-proved positivity of the five-flavor pole factor.
Claim. Let $m_{MS} > 0$ and $0 < α_s < 0.5$. Then the pole mass $m_{pole}$ obtained from the two-loop conversion formula at five light flavors satisfies $m_{pole} > 0$.
background
The module supplies the two-loop pole-to-MS-bar conversion for quarks, with the explicit relation $m_{pole} = m_{MS} × (1 + (4/3)(α_s/π) + K_2 (α_s/π)^2 + O(α_s^3))$ where $K_2 ≈ 5.9$ for the top quark at five light flavors. The function m_pole_from_MS multiplies the input MS-bar mass by the pole factor that encodes these coefficients. Upstream lemmas establish the one-loop coefficient K_1 and the positivity of the pole factor at five flavors under the stated bounds on α_s.
proof idea
The proof is a one-line term-mode wrapper. It unfolds the definition of m_pole_from_MS and applies the multiplication-positivity lemma directly to the hypothesis that the MS-bar mass is positive together with the positivity of the pole factor at five flavors.
why it matters
This lemma is invoked inside poleToMSbarCert_holds, which assembles the full set of positivity and equality facts for the conversion. It is also applied directly to establish positivity of the predicted top pole mass in the TopMSBarScoreCard module. Within the Recognition Science framework it closes the positivity requirement for the top-quark mass entry on the phi-ladder before comparison with experimental pole-mass values.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.