mZ

formal source

  56def mW (g v : ℝ) : ℝ := Real.sqrt (mW_sq g v)
  57
  58/-- Z boson mass: `m_Z = √(g² + g'²) · v / 2` (for `g, g', v > 0`). -/
  59def mZ (g gp v : ℝ) : ℝ := Real.sqrt (mZ_sq g gp v)
  60
  61/-- `m_W² ≥ 0` always. -/
  62theorem mW_sq_nonneg (g v : ℝ) : 0 ≤ mW_sq g v := by
  63  unfold mW_sq
  64  have h1 : 0 ≤ g ^ 2 := sq_nonneg _
  65  have h2 : 0 ≤ v ^ 2 := sq_nonneg _
  66  positivity
  67
  68/-- `m_Z² ≥ 0` always. -/
  69theorem mZ_sq_nonneg (g gp v : ℝ) : 0 ≤ mZ_sq g gp v := by
  70  unfold mZ_sq
  71  have h1 : 0 ≤ g ^ 2 := sq_nonneg _
  72  have h2 : 0 ≤ gp ^ 2 := sq_nonneg _
  73  have h3 : 0 ≤ v ^ 2 := sq_nonneg _
  74  have hsum : 0 ≤ g ^ 2 + gp ^ 2 := by linarith
  75  positivity
  76
  77/-- `m_W² ≤ m_Z²` for any `g, g', v` (since `g'² ≥ 0`). -/
  78theorem mW_sq_le_mZ_sq (g gp v : ℝ) : mW_sq g v ≤ mZ_sq g gp v := by
  79  unfold mW_sq mZ_sq
  80  have hgp : 0 ≤ gp ^ 2 := sq_nonneg _
  81  have hv2 : 0 ≤ v ^ 2 := sq_nonneg _
  82  have hprod : 0 ≤ gp ^ 2 * v ^ 2 := mul_nonneg hgp hv2
  83  nlinarith [hprod]
  84
  85/-- The Z is heavier than the W when `g'` is non-trivial, i.e. when
  86    electromagnetic mixing is present. -/
  87theorem mW_sq_lt_mZ_sq_of_gp_pos (g gp v : ℝ) (hgp : 0 < gp) (hv : 0 < v) :
  88    mW_sq g v < mZ_sq g gp v := by
  89  unfold mW_sq mZ_sq