IndisputableMonolith.StandardModel.ElectroweakMassBridge

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.StandardModel.HiggsEFTBridge
   4
   5/-!
   6# Electroweak Mass Bridge
   7
   8This module derives the Standard-Model gauge-boson mass relations from the
   9recognition-substrate scale `v` plus generic positive gauge couplings
  10`g, g'`.  Concretely it formalises
  11
  12    m_W² = g² v² / 4,
  13    m_Z² = (g² + g'²) v² / 4,
  14    m_W / m_Z = cos θ_W = g / √(g² + g'²),
  15    sin² θ_W = g'² / (g² + g'²).
  16
  17These are the SM tree-level gauge-mass relations.  Their content here is
  18conditional: given the same `v` from the RS substrate (formalised in
  19`HiggsEFTBridge`) and any positive `g, g'`, the SM gauge-mass relations
  20hold.  The identification of `g, g'` with their measured numerical values
  21remains an empirical input, just as the φ-ladder numerical match for `v`
  22is a separate (still open) calibration step.
  23
  24The companion module `Masses/ElectroweakMasses.lean` already provides a
  25recognition-Weinberg-angle prediction `sin²θ_W = (3 − φ)/6` and proves
  26`w_pred / z_pred = cos θ_W` on its specific RS yardsticks.  The present
  27module instead proves the *gauge relation* unconditionally on positive
  28`(g, g')`, so any definition of `θ_W` (RS or PDG) is admissible as input.
  29
  30## Status
  31
  32* `THEOREM`: all gauge-mass relations on positive `(g, g', v)`.
  33* `THEOREM`: the W/Z ratio equals `cos θ_W` from the SM definition.
  34* `OPEN`: numerical calibration of `g, g'` from RS substrate (separate
  35  from this bridge; tracked under the `OPEN_NORMALIZATION` tag).
  36-/
  37
  38namespace IndisputableMonolith
  39namespace StandardModel
  40namespace ElectroweakMassBridge
  41
  42open Real
  43open Constants
  44
  45noncomputable section
  46
  47/-! ## §1. Tree-Level Gauge-Boson Masses -/
  48
  49/-- W boson mass squared: `m_W² = g² v² / 4`. -/
  50def mW_sq (g v : ℝ) : ℝ := g ^ 2 * v ^ 2 / 4
  51
  52/-- Z boson mass squared: `m_Z² = (g² + g'²) v² / 4`. -/
  53def mZ_sq (g gp v : ℝ) : ℝ := (g ^ 2 + gp ^ 2) * v ^ 2 / 4
  54
  55/-- W boson mass: `m_W = g v / 2` (for `g, v > 0`). -/
  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
  90  have hv2 : 0 < v ^ 2 := by positivity
  91  have hgp2 : 0 < gp ^ 2 := by positivity
  92  have hprod : 0 < gp ^ 2 * v ^ 2 := mul_pos hgp2 hv2
  93  nlinarith [hprod]
  94
  95/-! ## §2. The W/Z Ratio Identity -/
  96
  97/-- The W/Z ratio identity in squared form:
  98
  99    m_W² / m_Z² = g² / (g² + g'²) = cos² θ_W. -/
 100theorem mW_over_mZ_sq (g gp v : ℝ) (hg : 0 < g) (hv : 0 < v) :
 101    mW_sq g v / mZ_sq g gp v = g ^ 2 / (g ^ 2 + gp ^ 2) := by
 102  unfold mW_sq mZ_sq
 103  have hg2 : 0 < g ^ 2 := by positivity
 104  have hgp2 : 0 ≤ gp ^ 2 := sq_nonneg _
 105  have hsum : 0 < g ^ 2 + gp ^ 2 := by linarith
 106  have hv2 : 0 < v ^ 2 := by positivity
 107  field_simp
 108
 109/-- The Standard-Model definition of `cos² θ_W` from gauge couplings. -/
 110def cos_sq_thetaW_SM (g gp : ℝ) : ℝ := g ^ 2 / (g ^ 2 + gp ^ 2)
 111
 112/-- The Standard-Model definition of `sin² θ_W` from gauge couplings. -/
 113def sin_sq_thetaW_SM (g gp : ℝ) : ℝ := gp ^ 2 / (g ^ 2 + gp ^ 2)
 114
 115/-- `cos²θ_W + sin²θ_W = 1` for nontrivial gauge couplings. -/
 116theorem cos_sq_plus_sin_sq_thetaW (g gp : ℝ) (hg : 0 < g) :
 117    cos_sq_thetaW_SM g gp + sin_sq_thetaW_SM g gp = 1 := by
 118  unfold cos_sq_thetaW_SM sin_sq_thetaW_SM
 119  have hg2 : 0 < g ^ 2 := by positivity
 120  have hgp2 : 0 ≤ gp ^ 2 := sq_nonneg _
 121  have hsum_pos : 0 < g ^ 2 + gp ^ 2 := by linarith
 122  have hsum_ne : g ^ 2 + gp ^ 2 ≠ 0 := ne_of_gt hsum_pos
 123  field_simp
 124
 125/-- The W/Z mass-squared ratio equals `cos² θ_W` in the SM definition. -/
 126theorem mW_over_mZ_sq_eq_cos_sq (g gp v : ℝ) (hg : 0 < g) (hv : 0 < v) :
 127    mW_sq g v / mZ_sq g gp v = cos_sq_thetaW_SM g gp := by
 128  rw [mW_over_mZ_sq g gp v hg hv]
 129  rfl
 130
 131/-- `cos²θ_W ∈ (0, 1]` for any nontrivial gauge coupling pair. -/
 132theorem cos_sq_thetaW_in_unit_interval (g gp : ℝ) (hg : 0 < g) :
 133    0 < cos_sq_thetaW_SM g gp ∧ cos_sq_thetaW_SM g gp ≤ 1 := by
 134  unfold cos_sq_thetaW_SM
 135  have hg2 : 0 < g ^ 2 := by positivity
 136  have hgp2 : 0 ≤ gp ^ 2 := sq_nonneg _
 137  have hsum_pos : 0 < g ^ 2 + gp ^ 2 := by linarith
 138  refine ⟨?_, ?_⟩
 139  · exact div_pos hg2 hsum_pos
 140  · rw [div_le_one hsum_pos]; linarith
 141
 142/-- The Z is heavier than (or equal to) the W in mass-squared. -/
 143theorem mZ_sq_ge_mW_sq (g gp v : ℝ) : mW_sq g v ≤ mZ_sq g gp v :=
 144  mW_sq_le_mZ_sq g gp v
 145
 146/-- The W/Z mass ratio identity in mass form (under positivity). -/
 147theorem mW_over_mZ_eq_cos_thetaW (g gp v : ℝ)
 148    (hg : 0 < g) (hgp : 0 ≤ gp) (hv : 0 < v) :
 149    mW g v / mZ g gp v = Real.sqrt (cos_sq_thetaW_SM g gp) := by
 150  unfold mW mZ
 151  have hmW_sq_pos : 0 < mW_sq g v := by
 152    unfold mW_sq; positivity
 153  have hmZ_sq_pos : 0 < mZ_sq g gp v := by
 154    unfold mZ_sq
 155    have hg2 : 0 < g ^ 2 := by positivity
 156    have hgp2 : 0 ≤ gp ^ 2 := sq_nonneg _
 157    have hsum : 0 < g ^ 2 + gp ^ 2 := by linarith
 158    have hv2 : 0 < v ^ 2 := by positivity
 159    positivity
 160  -- Use Real.sqrt_div_sqrt-style identity via Real.sqrt_div'
 161  have hmW_nn : 0 ≤ mW_sq g v := le_of_lt hmW_sq_pos
 162  have hmZ_nn : 0 ≤ mZ_sq g gp v := le_of_lt hmZ_sq_pos
 163  rw [← Real.sqrt_div hmW_nn]
 164  congr 1
 165  exact mW_over_mZ_sq_eq_cos_sq g gp v hg hv
 166
 167/-! ## §3. Master Bridge Certificate -/
 168
 169/-- Master certificate for the W/Z mass relations.
 170
 171    Tags:
 172    - `THEOREM`: all clauses are unconditional theorems on positive
 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
 207end
 208
 209end ElectroweakMassBridge
 210end StandardModel
 211end IndisputableMonolith
 212