structure
definition
HiggsRungCert
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.StandardModel.HiggsRungAssignment on GitHub at line 196.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
of -
rung -
rung -
contains -
of -
is -
of -
from -
is -
of -
is -
of -
rung -
rung -
is -
and -
contains -
rung -
higgs_rung_from_prediction -
mH_obs -
mH_rs_level2 -
mH_rs_level3 -
sin2ThetaW_RS -
w_rung
used by
formal source
193
194/-! ## Summary Certificate -/
195
196structure HiggsRungCert where
197 /-- sin²θ_W = (3-φ)/6 (from WeinbergAngle) -/
198 weinberg_angle : 0.228 < sin2ThetaW_RS ∧ sin2ThetaW_RS < 0.232
199 /-- Level 2 prediction in (110, 125) -/
200 level2_range : 110 < mH_rs_level2 ∧ mH_rs_level2 < 125
201 /-- Level 3 prediction in (120, 130) — contains 125.2 GeV -/
202 level3_range : 120 < mH_rs_level3 ∧ mH_rs_level3 < 130
203 /-- Higgs rung is between 21 and 22 -/
204 higgs_rung_range : (w_rung : ℝ) < higgs_rung_from_prediction ∧
205 higgs_rung_from_prediction < (w_rung : ℝ) + 1
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