`electroweakMassBridgeCert`

definition

show as: view math explainer →

module: IndisputableMonolith.StandardModel.ElectroweakMassBridge
domain: StandardModel
line: 195 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.StandardModel.ElectroweakMassBridge on GitHub at line 195.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 192  cos_sq_window    : ∀ g gp, 0 < g →
 193    0 < cos_sq_thetaW_SM g gp ∧ cos_sq_thetaW_SM g gp ≤ 1
 194
 195def electroweakMassBridgeCert : ElectroweakMassBridgeCert where
 196  mW_sq_nn         := mW_sq_nonneg
 197  mZ_sq_nn         := mZ_sq_nonneg
 198  mW_le_mZ         := mW_sq_le_mZ_sq
 199  mW_lt_mZ         := fun g gp v hgp hv => mW_sq_lt_mZ_sq_of_gp_pos g gp v hgp hv
 200  ratio_eq_cos_sq  := fun g gp v hg hv => mW_over_mZ_sq_eq_cos_sq g gp v hg hv
 201  cos2_plus_sin2   := fun g gp hg => cos_sq_plus_sin_sq_thetaW g gp hg
 202  cos_sq_window    := fun g gp hg => cos_sq_thetaW_in_unit_interval g gp hg
 203
 204theorem electroweakMassBridgeCert_inhabited : Nonempty ElectroweakMassBridgeCert :=
 205  ⟨electroweakMassBridgeCert⟩
 206
 207end
 208
 209end ElectroweakMassBridge
 210end StandardModel
 211end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.