module module

`IndisputableMonolith.StandardModel.ElectroweakMassBridge`

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 (3)

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

IndisputableMonolith module_import
IndisputableMonolith.StandardModel.HiggsEFTLowEnergyLimit module_import
IndisputableMonolith.StandardModel.LongitudinalVectorScattering module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.StandardModel.HiggsEFTBridge module_import

declarations in this module (19)

def mW_sq L50
def mZ_sq L53
def mW L56
def mZ L59
theorem mW_sq_nonneg L62
theorem mZ_sq_nonneg L69
theorem mW_sq_le_mZ_sq L78
theorem mW_sq_lt_mZ_sq_of_gp_pos L87
theorem mW_over_mZ_sq L100
def cos_sq_thetaW_SM L110
def sin_sq_thetaW_SM L113
theorem cos_sq_plus_sin_sq_thetaW L116
theorem mW_over_mZ_sq_eq_cos_sq L126
theorem cos_sq_thetaW_in_unit_interval L132
theorem mZ_sq_ge_mW_sq L143
theorem mW_over_mZ_eq_cos_thetaW L147
structure ElectroweakMassBridgeCert L176
def electroweakMassBridgeCert L195
theorem electroweakMassBridgeCert_inhabited L204