structure
definition
TopQuarkMassScoreCardCert
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Masses.TopQuarkMassScoreCard on GitHub at line 47.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
44theorem row_top_in_band_scorecard : (10000 : ℝ) < top_quark_pred ∧ top_quark_pred < 1000000 :=
45 row_top_quark_in_band
46
47structure TopQuarkMassScoreCardCert where
48 positive : 0 < top_quark_pred
49 top_charm : top_quark_pred / charm_quark_pred = phi ^ (6 : ℕ)
50 order_MeV : (10000 : ℝ) < top_quark_pred ∧ top_quark_pred < 1000000
51 pdg_ref_pos : 0 < row_pdg_top_MeV
52
53theorem topQuarkMassScoreCardCert_holds : Nonempty TopQuarkMassScoreCardCert :=
54 ⟨{ positive := row_top_pos
55 top_charm := row_top_charm
56 order_MeV := row_top_order_MeV
57 pdg_ref_pos := row_pdg_top_positive }⟩
58
59end
60
61end IndisputableMonolith.Masses.TopQuarkMassScoreCard