IndisputableMonolith.Physics.TopMSBarScoreCard

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Physics.QCDRGE.TwoLoopAlphaS
   4import IndisputableMonolith.Physics.QCDRGE.MassAnomalousDimension
   5import IndisputableMonolith.Physics.QCDRGE.PoleToMSbar
   6
   7/-!
   8# Top Quark Pole / MS-bar Mass Scorecard
   9
  10PDG 2024: m_t (pole) = 172.69 +- 0.30 GeV.
  11RS sector rung t = 21 (up-type, generation 3).
  12
  13Note: PDG reports the top quark mass as the pole mass (with a recent shift
  14towards the MS-bar version). We expose both forms.
  15
  16## Status: 0 sorry, 0 axiom.
  17-/
  18
  19namespace IndisputableMonolith.Physics.TopMSBarScoreCard
  20
  21open Constants
  22open IndisputableMonolith.Physics.QCDRGE.TwoLoopAlphaS
  23open IndisputableMonolith.Physics.QCDRGE.MassAnomalousDimension
  24open IndisputableMonolith.Physics.QCDRGE.PoleToMSbar
  25
  26noncomputable section
  27
  28def m_t_pole_PDG_GeV : ℝ := 172.69
  29def m_t_pole_PDG_unc_GeV : ℝ := 0.30
  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
  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
  74    prediction_pos := m_t_pole_predicted_pos }
  75
  76end
  77
  78end IndisputableMonolith.Physics.TopMSBarScoreCard
  79