row_fermi_codata_in_bracket

formal source

  95    (1.16e-5 : ℝ) < row_fermi_pred ∧ row_fermi_pred < (1.17e-5 : ℝ) :=
  96  ⟨row_fermi_pred_lower, row_fermi_pred_upper⟩
  97
  98theorem row_fermi_codata_in_bracket :
  99    (1.16e-5 : ℝ) < row_fermi_codata ∧ row_fermi_codata < (1.17e-5 : ℝ) := by
 100  unfold row_fermi_codata
 101  constructor <;> norm_num
 102
 103structure FermiConstantScoreCardCert where
 104  fermi_bracket :
 105    (1.16e-5 : ℝ) < row_fermi_pred ∧ row_fermi_pred < (1.17e-5 : ℝ)
 106  codata_in_bracket :
 107    (1.16e-5 : ℝ) < row_fermi_codata ∧ row_fermi_codata < (1.17e-5 : ℝ)
 108  vev_range : (244 : ℝ) < vev_canonical ∧ vev_canonical < (248 : ℝ)
 109
 110theorem fermiConstantScoreCardCert_holds :
 111    Nonempty FermiConstantScoreCardCert :=
 112  ⟨{ fermi_bracket := row_fermi_pred_bracket
 113     codata_in_bracket := row_fermi_codata_in_bracket
 114     vev_range := vev_in_range }⟩
 115
 116end
 117
 118end IndisputableMonolith.Constants.FermiConstantScoreCard