ElectroweakMassBridgeCert

formal source

 173      gauge couplings and positive electroweak scale.
 174    - `OPEN_NORMALIZATION`: deriving `g, g'` numerically from the RS
 175      substrate is a separate problem, not closed here. -/
 176structure ElectroweakMassBridgeCert where
 177  /-- THEOREM: m_W² ≥ 0 unconditionally. -/
 178  mW_sq_nn         : ∀ g v, 0 ≤ mW_sq g v
 179  /-- THEOREM: m_Z² ≥ 0 unconditionally. -/
 180  mZ_sq_nn         : ∀ g gp v, 0 ≤ mZ_sq g gp v
 181  /-- THEOREM: m_W² ≤ m_Z² unconditionally. -/
 182  mW_le_mZ         : ∀ g gp v, mW_sq g v ≤ mZ_sq g gp v
 183  /-- THEOREM: m_W² < m_Z² when `g'` is nontrivial. -/
 184  mW_lt_mZ         : ∀ g gp v, 0 < gp → 0 < v → mW_sq g v < mZ_sq g gp v
 185  /-- THEOREM: the W/Z mass-squared ratio equals `cos²θ_W`. -/
 186  ratio_eq_cos_sq  : ∀ g gp v, 0 < g → 0 < v →
 187    mW_sq g v / mZ_sq g gp v = cos_sq_thetaW_SM g gp
 188  /-- THEOREM: cos²θ_W + sin²θ_W = 1. -/
 189  cos2_plus_sin2   : ∀ g gp, 0 < g →
 190    cos_sq_thetaW_SM g gp + sin_sq_thetaW_SM g gp = 1
 191  /-- THEOREM: `cos²θ_W` lies in `(0, 1]`. -/
 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