  77    norm_num
  78  nlinarith
  79
  80theorem row_fermi_pred_upper :
  81    row_fermi_pred < (1.17e-5 : ℝ) := by
  82  unfold row_fermi_pred
  83  rw [div_lt_iff₀ fermi_den_pos]
  84  have hs : (1.4142 : ℝ) < Real.sqrt 2 := sqrt2_gt_14142
  85  have hden :
  86      (1.4142 : ℝ) * (246 : ℝ) ^ 2 < Real.sqrt 2 * vev_canonical ^ 2 := by
  87    have hv : vev_canonical = (246 : ℝ) := rfl
  88    rw [hv]
  89    nlinarith
  90  have hnum : 1 < (1.17e-5 : ℝ) * ((1.4142 : ℝ) * (246 : ℝ) ^ 2) := by
  91    norm_num
  92  nlinarith
  93
  94theorem row_fermi_pred_bracket :
  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 :

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.