r_bottom

formal source

  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