theorem
proved
d_2_mass_neg
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Physics.QCDRGE.ThresholdMatching on GitHub at line 121.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
118 0 < mass_match mass_above alpha_at_threshold
119
120theorem c_2_alpha_pos : 0 < c_2_alpha := by unfold c_2_alpha; norm_num
121theorem d_2_mass_neg : d_2_mass < 0 := by unfold d_2_mass; norm_num
122
123theorem thresholdMatchingCert_holds : ThresholdMatchingCert :=
124 { c_2_alpha_pos := c_2_alpha_pos
125 d_2_mass_neg := d_2_mass_neg
126 alpha_match_pos_lemma := alpha_match_pos
127 mass_match_pos_lemma := mass_match_pos }
128
129end
130
131end IndisputableMonolith.Physics.QCDRGE.ThresholdMatching