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