pith. machine review for the scientific record. sign in
theorem

higgsRungCert

proved
show as:
view math explainer →
module
IndisputableMonolith.StandardModel.HiggsRungAssignment
domain
StandardModel
line
209 · github
papers citing
none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.StandardModel.HiggsRungAssignment on GitHub at line 209.

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

 206  /-- Within 5% of observed -/
 207  within_5_percent : |mH_rs_level3 - mH_obs| / mH_obs < 0.05
 208
 209theorem higgsRungCert : HiggsRungCert where
 210  weinberg_angle := sin2ThetaW_RS_approx
 211  level2_range := mH_rs_level2_in_range
 212  level3_range := mH_prediction_in_interval
 213  higgs_rung_range := higgs_rung_in_range
 214  within_5_percent := mH_within_5_percent_of_observed
 215
 216end
 217end HiggsRungAssignment
 218end StandardModel
 219end IndisputableMonolith