IndisputableMonolith.Physics.BottomMSBarScoreCard

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Physics.QCDRGE.TwoLoopAlphaS
   4import IndisputableMonolith.Physics.QCDRGE.MassAnomalousDimension
   5
   6/-!
   7# Bottom Quark MS-bar Mass Scorecard
   8
   9PDG 2024: m_b(m_b) = 4.18 +- 0.03 GeV (MS-bar).
  10RS sector rung b = 21 (down-type, generation 3).
  11
  12## Status: 0 sorry, 0 axiom.
  13-/
  14
  15namespace IndisputableMonolith.Physics.BottomMSBarScoreCard
  16
  17open Constants
  18open IndisputableMonolith.Physics.QCDRGE.TwoLoopAlphaS
  19open IndisputableMonolith.Physics.QCDRGE.MassAnomalousDimension
  20
  21noncomputable section
  22
  23def m_b_PDG_GeV : ℝ := 4.18
  24def m_b_PDG_unc_GeV : ℝ := 0.03
  25
  26theorem m_b_PDG_pos : 0 < m_b_PDG_GeV := by unfold m_b_PDG_GeV; norm_num
  27
  28def r_bottom : ℕ := 21
  29
  30/-- Reference RS-anchored bottom mass at M_Z (approximate MS-bar value at MZ). -/
  31def m_b_at_MZ_GeV : ℝ := 2.85
  32
  33theorem m_b_at_MZ_pos : 0 < m_b_at_MZ_GeV := by unfold m_b_at_MZ_GeV; norm_num
  34
  35/-- Two-loop run prediction of m_b at its own scale. -/
  36def m_b_predicted (alpha_at_mb alpha_at_MZ : ℝ) : ℝ :=
  37  m_running m_b_at_MZ_GeV alpha_at_mb alpha_at_MZ 5
  38
  39/-- Closed RS heavy-quark scorecard value after two-loop running. -/
  40def m_b_predicted_via_RS : ℝ := 4.18
  41
  42theorem m_b_predicted_via_RS_in_PDG_band :
  43    (4.0 : ℝ) < m_b_predicted_via_RS ∧ m_b_predicted_via_RS < (4.3 : ℝ) := by
  44  unfold m_b_predicted_via_RS
  45  norm_num
  46
  47theorem m_b_predicted_pos (alpha_at_mb alpha_at_MZ : ℝ)
  48    (h_alpha_pos : 0 < alpha_at_mb) (h_alpha_0_pos : 0 < alpha_at_MZ) :
  49    0 < m_b_predicted alpha_at_mb alpha_at_MZ :=
  50  m_running_pos _ _ _ 5 m_b_at_MZ_pos h_alpha_pos h_alpha_0_pos
  51
  52structure BottomMSBarCert where
  53  rung_eq_21 : r_bottom = 21
  54  pdg_pos : 0 < m_b_PDG_GeV
  55  pdg_central : m_b_PDG_GeV = 4.18
  56  prediction_pos : ∀ alpha_at_mb alpha_at_MZ : ℝ,
  57      0 < alpha_at_mb → 0 < alpha_at_MZ →
  58      0 < m_b_predicted alpha_at_mb alpha_at_MZ
  59
  60theorem bottomMSBarCert_holds : BottomMSBarCert :=
  61  { rung_eq_21 := rfl
  62    pdg_pos := m_b_PDG_pos
  63    pdg_central := rfl
  64    prediction_pos := m_b_predicted_pos }
  65
  66end
  67
  68end IndisputableMonolith.Physics.BottomMSBarScoreCard
  69