`row_mH_codata_pos`

proved

show as: view math explainer →

module: IndisputableMonolith.Physics.HiggsMassScoreCard
domain: Physics
line: 32 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Physics.HiggsMassScoreCard on GitHub at line 32.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  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

papers checked against this theorem

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