pith. machine review for the scientific record. sign in
structure definition def or abbrev

ElectroweakMassBridgeCert

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

formal statement (Lean)

 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

used by (3)

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

depends on (14)

Lean names referenced from this declaration's body.