spin0_casimir
open lean source
IndisputableMonolith.StandardModel.Q3Representations on GitHub at line 91.
browse module
All declarations in this module, on Recognition.
plain-language theorem explainer
Spin-0 Casimir eigenvalue vanishes under the definition C₂ = j(j + 1). Recognition Science analyses of electroweak symmetry breaking cite this when isolating the potential curvature contribution to the Higgs mass. The term-mode proof applies simplification directly to the casimir definition.
Claim. $C_2(0) = 0$ where $C_2(j) = j(j+1)$ is the Casimir eigenvalue for the spin-$j$ representation of $Q_3$.
background
The Q3Representations module formalizes the quaternion group Q3 as the symmetry group of the eight-tick cycle in Recognition Science. Under SU(2)×U(1) → U(1) breaking the Higgs doublet splits into one physical spin-0 mode and three spin-1 Goldstone modes. The upstream Spin structure from SpinStatistics encodes the quantum number as a non-negative integer via its twice field. The sibling casimir definition returns the standard eigenvalue j(j+1) for natural-number j.
proof idea
The proof is a one-line wrapper that applies the definition of casimir via the simp tactic.
why it matters
This result is invoked by the downstream casimir_ratio_undefined theorem, which states that the spin-1 to spin-0 Casimir ratio is undefined and that the physical mass ratio instead follows from the quartic coupling λ_RS = J''(1)/2 = 1/2. The module documentation ties the construction to the eight-tick octave and the forced J-cost potential curvature rather than representation theory alone.
depends on
used by
formal source
88noncomputable def casimir (j : ℕ) : ℝ := (j : ℝ) * ((j : ℝ) + 1)
89
90/-- Spin-0 Casimir eigenvalue: j=0, C₂ = 0. -/
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