def
definition
m_t_pole_predicted_via_RS
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.TopMSBarScoreCard on GitHub at line 47.
browse module
All declarations in this module, on Recognition.
explainer page
used by
formal source
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