m_b_predicted_pos

formal source

  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