m_t_pole_predicted
plain-language theorem explainer
The definition supplies the RS-predicted top-quark pole mass as a function of the strong coupling at the top scale. QCD phenomenologists comparing the Recognition Science mass ladder to lattice or effective-field-theory results would cite it when checking consistency with the PDG central value. It is realized as a direct call to the two-loop pole conversion applied to the fixed MS-bar anchor of 162.5 GeV with five active flavors.
Claim. Let $m_t^{MS}(m_t)=162.5$ GeV be the RS-anchored MS-bar mass at the top scale. The predicted pole mass is $m_t^{pole}=m_t^{MS}(m_t)×F(α_s(m_t),5)$, where $F$ denotes the two-loop pole conversion factor for five light flavors.
background
The Top Quark Pole / MS-bar Mass Scorecard module places the top quark at rung 21 on the phi-ladder (up-type, generation 3) and records the PDG 2024 pole-mass central value 172.69 GeV. The module exposes both pole and MS-bar forms, with the latter fixed at the approximate value 162.5 GeV. The conversion from MS-bar mass at its own scale to pole mass multiplies the MS-bar value by the perturbative pole factor that depends on the strong coupling and the number of light flavors.
proof idea
The definition is a one-line wrapper that applies the pole-mass conversion function to the constant MS-bar reference 162.5 GeV, the input coupling, and five light flavors.
why it matters
This definition supplies the numerical prediction that enters the positivity theorem for the predicted pole mass and the TopMSBarCert certification structure. It realizes the RS mass formula at rung 21 for the top quark, enabling direct comparison against the experimental pole mass inside the alpha band. The construction closes the scorecard for the heaviest quark without new axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.