vev_GeV

formal source

  53def zBosonMass_GeV : ℝ := 91.1876
  54
  55/-- Higgs VEV in GeV. -/
  56def vev_GeV : ℝ := 246.22
  57
  58/-- Weak mixing angle sin²θW (on-shell scheme). -/
  59def sin2_theta_W : ℝ := 0.23122
  60
  61/-- Cos θW from sin²θW. -/
  62def cos_theta_W : ℝ := sqrt (1 - sin2_theta_W)
  63
  64/-! ## Mass Relations -/
  65
  66/-- W/Z mass ratio. -/
  67def wz_mass_ratio : ℝ := wBosonMass_GeV / zBosonMass_GeV
  68
  69/-- Predicted W/Z ratio = cos(θW). -/
  70theorem wz_ratio_equals_cos_theta :
  71    |wz_mass_ratio - cos_theta_W| < 0.005 := by
  72  -- wz_mass_ratio = 80.3692 / 91.1876 ≈ 0.88136
  73  -- cos_theta_W = sqrt(1 - 0.23122) = sqrt(0.76878) ≈ 0.87683
  74  -- |0.88136 - 0.87683| = 0.00453 < 0.005
  75  simp only [wz_mass_ratio, wBosonMass_GeV, zBosonMass_GeV, cos_theta_W, sin2_theta_W]
  76  -- Need: |80.3692/91.1876 - sqrt(0.76878)| < 0.005
  77  -- Bounds on ratio: 0.8813 < ratio < 0.8814
  78  have h_ratio_lo : (80.3692 : ℝ) / 91.1876 > 0.8813 := by norm_num
  79  have h_ratio_hi : (80.3692 : ℝ) / 91.1876 < 0.8814 := by norm_num
  80  -- Bounds on sqrt: 0.8768 < sqrt(0.76878) < 0.8769
  81  -- 0.8768^2 = 0.76877824, 0.8769^2 = 0.76895361
  82  have h_sqrt_lo : sqrt 0.76878 > 0.8768 := by
  83    have h_sq : (0.8768 : ℝ)^2 < 0.76878 := by norm_num
  84    exact (Real.lt_sqrt (by norm_num : (0 : ℝ) ≤ 0.8768)).mpr h_sq
  85  have h_sqrt_hi : sqrt 0.76878 < 0.8769 := by
  86    have h_sq : 0.76878 < (0.8769 : ℝ)^2 := by norm_num