m_t_MS_at_mt_GeV
plain-language theorem explainer
The declaration supplies the reference MS-bar mass for the top quark at its own scale, fixed at 162.5 GeV within the Recognition Science framework. Researchers comparing pole and running masses for heavy quarks would reference this value when applying two-loop QCD running and pole conversion formulas. It is introduced as a direct numeric constant with no computation or lemmas required.
Claim. Let $m_t^{MS}(m_t)$ denote the MS-bar mass of the top quark evaluated at the top-quark mass scale. Then $m_t^{MS}(m_t) = 162.5$ GeV.
background
The Top Quark Pole / MS-bar Mass Scorecard module assigns the top quark to rung t = 21 on the phi-ladder for the up-type third generation. It contrasts the PDG 2024 pole mass of 172.69 +- 0.30 GeV with an RS-anchored MS-bar reference at the m_t scale, noting that PDG reports the pole mass while the module exposes both forms. This definition provides the central MS-bar value used for subsequent pole-mass predictions via m_pole_from_MS with N_l = 5 light flavors.
proof idea
The definition is a direct numeric assignment of the real number 162.5 with no lemmas applied.
why it matters
This constant anchors the closed RS heavy-quark scorecard value after two-loop running and pole conversion, as seen in the downstream definition m_t_pole_predicted. It supports the TopMSBarCert structure that certifies consistency with the rung-21 assignment and PDG data. The value lies within the approximate 162-163 GeV band noted for RS-native units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.