structure
definition
CharmMSBarCert
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Physics.CharmMSBarScoreCard on GitHub at line 89.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
86
87/-! ## Master cert -/
88
89structure CharmMSBarCert where
90 rung_eq_15 : r_charm = 15
91 pdg_pos : 0 < m_c_PDG_GeV
92 pdg_central : m_c_PDG_GeV = 1.27
93 prediction_pos : ∀ alpha_at_mc alpha_at_MZ : ℝ,
94 0 < alpha_at_mc → 0 < alpha_at_MZ →
95 0 < m_c_predicted alpha_at_mc alpha_at_MZ
96
97theorem charmMSBarCert_holds : CharmMSBarCert :=
98 { rung_eq_15 := rfl
99 pdg_pos := m_c_PDG_pos
100 pdg_central := rfl
101 prediction_pos := m_c_predicted_pos }
102
103end
104
105end IndisputableMonolith.Physics.CharmMSBarScoreCard