row_mH_codata

formal source

  27
  28noncomputable section
  29
  30noncomputable def row_mH_codata : ℝ := mH_obs
  31
  32theorem row_mH_codata_pos : 0 < row_mH_codata := by
  33  unfold row_mH_codata mH_obs
  34  norm_num
  35
  36theorem row_mH_pred_interval :
  37    120 < mH_rs_level3 ∧ mH_rs_level3 < 130 := mH_prediction_in_interval
  38
  39theorem row_mH_within_five_percent :
  40    |mH_rs_level3 - row_mH_codata| / row_mH_codata < 0.05 := by
  41  simpa [row_mH_codata] using mH_within_5_percent_of_observed
  42
  43structure HiggsMassScoreCardCert where
  44  mass_interval : 120 < mH_rs_level3 ∧ mH_rs_level3 < 130
  45  five_percent : |mH_rs_level3 - mH_obs| / mH_obs < 0.05
  46
  47theorem higgsMassScoreCardCert_holds : Nonempty HiggsMassScoreCardCert :=
  48  ⟨{ mass_interval := row_mH_pred_interval
  49     five_percent := mH_within_5_percent_of_observed }⟩
  50
  51end
  52
  53end IndisputableMonolith.Physics.HiggsMassScoreCard