theorem
proved
higgsRungCert
show as:
view math explainer →
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
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