pith. machine review for the scientific record. sign in
def definition def or abbrev high

m_t_pole_predicted

show as:
view Lean formalization →

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.

claimLet $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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  43def m_t_pole_predicted (alpha_at_mt : ℝ) : ℝ :=

proof body

Definition body.

  44  m_pole_from_MS m_t_MS_at_mt_GeV alpha_at_mt 5
  45
  46/-- Closed RS heavy-quark scorecard value after two-loop running and pole conversion. -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (5)

Lean names referenced from this declaration's body.