module module

`IndisputableMonolith.StandardModel.HiggsRungAssignment`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Physics.HiggsMassScoreCard module_import

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.StandardModel.Q3Representations module_import
IndisputableMonolith.StandardModel.WeinbergAngle module_import

declarations in this module (17)

def vev L60
def mW_obs L63
def mZ_obs L66
def mH_obs L69
theorem vev_pos L72
def mH_naive L78
def mH_rs_level2 L82
theorem mH_rs_level2_in_range L86
def mH_rs_level3 L109
theorem q3_correction_pos L113
theorem mH_rs_level3_pos L117
theorem mH_prediction_in_interval L126
def higgs_rung_from_prediction L158
theorem higgs_rung_in_range L162
theorem mH_within_5_percent_of_observed L187
structure HiggsRungCert L196
theorem higgsRungCert L209