m_t_pole_predicted

formal source

  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
  64  ms_at_mt_pos : 0 < m_t_MS_at_mt_GeV
  65  prediction_pos : ∀ alpha_at_mt : ℝ,
  66      0 < alpha_at_mt → alpha_at_mt < 0.5 →
  67      0 < m_t_pole_predicted alpha_at_mt
  68
  69theorem topMSBarCert_holds : TopMSBarCert :=
  70  { rung_eq_21 := rfl
  71    pdg_pos := m_t_pole_PDG_pos
  72    pdg_central := rfl
  73    ms_at_mt_pos := m_t_MS_at_mt_pos