spin1_casimir

formal source

  91theorem spin0_casimir : casimir 0 = 0 := by simp [casimir]
  92
  93/-- Spin-1 Casimir eigenvalue: j=1, C₂ = 2. -/
  94theorem spin1_casimir : casimir 1 = 2 := by unfold casimir; norm_num
  95
  96/-- Casimir eigenvalue ratio (spin-1 to spin-0) is undefined (C₂=0 for spin-0).
  97    The mass ratio comes from the POTENTIAL curvature, not the Casimir directly. -/
  98theorem casimir_ratio_undefined : casimir 0 = 0 := spin0_casimir
  99
 100/-! ## The Correct Mass Ratio Derivation -/
 101
 102/-- The φ-forced quartic coupling: λ = J″(1)/2 = 1/2.
 103    J(x) = ½(x + x⁻¹) - 1 → J″(1) = 1 → λ_RS = J″(1)/2 = 1/2. -/
 104noncomputable def lambda_RS : ℝ := 1 / 2
 105
 106theorem lambda_RS_val : lambda_RS = 1 / 2 := rfl
 107
 108/-- The Higgs mass squared from the Mexican hat potential: m_H² = 2λv².
 109    With λ = 1/2: m_H² = v². -/
 110noncomputable def higgsMassSq_over_vev (v : ℝ) : ℝ := 2 * lambda_RS * v^2
 111
 112theorem higgsMassSq_simplifies (v : ℝ) :
 113    higgsMassSq_over_vev v = v^2 := by
 114  unfold higgsMassSq_over_vev lambda_RS; ring
 115
 116/-- The W-boson mass squared: m_W² = g²v²/4 where g is the SU(2) coupling.
 117    In RS: g² = 4 sin²θ_W · (mZ/v)² where sin²θ_W = (3-φ)/6 (proved elsewhere). -/
 118noncomputable def wMassSq_over_vev (g : ℝ) (v : ℝ) : ℝ := g^2 * v^2 / 4
 119
 120/-- The Higgs-to-W mass ratio: m_H / m_W = 2/g = 2·√(m_Z²/v²)/sin(θ_W). -/
 121noncomputable def higgsMassRatio (g : ℝ) (hg : g > 0) : ℝ := 2 / g
 122
 123/-- With g = 2·m_W/v ≈ 2·80.4/246 ≈ 0.654:
 124    m_H / m_W = 2/g ≈ 2/0.654 ≈ 3.06 ... but observed is 125.2/80.4 ≈ 1.557.