ThresholdMatchingCert

formal source

 108
 109/-! ## Master cert -/
 110
 111structure ThresholdMatchingCert where
 112  c_2_alpha_pos : 0 < c_2_alpha
 113  d_2_mass_neg : d_2_mass < 0
 114  alpha_match_pos_lemma : ∀ alpha_above : ℝ,
 115      0 < alpha_above → alpha_above < 1 → 0 < alpha_match alpha_above
 116  mass_match_pos_lemma : ∀ mass_above alpha_at_threshold : ℝ,
 117      0 < mass_above → 0 < alpha_at_threshold → alpha_at_threshold < 1 →
 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