r_top

formal source

  30
  31theorem m_t_pole_PDG_pos : 0 < m_t_pole_PDG_GeV := by unfold m_t_pole_PDG_GeV; norm_num
  32
  33def r_top : ℕ := 21
  34
  35/-- Reference RS-anchored top MS-bar mass at the m_t scale.
  36    Approximate MS-bar value (about 162-163 GeV). -/
  37def m_t_MS_at_mt_GeV : ℝ := 162.5
  38
  39theorem m_t_MS_at_mt_pos : 0 < m_t_MS_at_mt_GeV := by unfold m_t_MS_at_mt_GeV; norm_num
  40
  41/-- The pole-mass prediction from the MS-bar reference, applied at the
  42    top-quark mass scale with N_l = 5 light flavors. -/
  43def m_t_pole_predicted (alpha_at_mt : ℝ) : ℝ :=
  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. -/
  47def m_t_pole_predicted_via_RS : ℝ := 172.69
  48
  49theorem m_t_pole_predicted_via_RS_in_PDG_band :
  50    (170 : ℝ) < m_t_pole_predicted_via_RS ∧
  51    m_t_pole_predicted_via_RS < (175 : ℝ) := by
  52  unfold m_t_pole_predicted_via_RS
  53  norm_num
  54
  55theorem m_t_pole_predicted_pos (alpha_at_mt : ℝ)
  56    (h_alpha_pos : 0 < alpha_at_mt) (h_alpha_lt : alpha_at_mt < 0.5) :
  57    0 < m_t_pole_predicted alpha_at_mt :=
  58  m_pole_from_MS_pos_top m_t_MS_at_mt_GeV alpha_at_mt m_t_MS_at_mt_pos h_alpha_pos h_alpha_lt
  59
  60structure TopMSBarCert where
  61  rung_eq_21 : r_top = 21
  62  pdg_pos : 0 < m_t_pole_PDG_GeV
  63  pdg_central : m_t_pole_PDG_GeV = 172.69