def
definition
Spin1Sector
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.StandardModel.Q3Representations on GitHub at line 71.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
68def Spin0Sector : List Q3Element := [Q3Element.pos_one, Q3Element.neg_one]
69
70/-- The spin-1 sector (gauge sector): {±i, ±j, ±k}. These become W±, Z. -/
71def Spin1Sector : List Q3Element :=
72 [Q3Element.pos_i, Q3Element.neg_i,
73 Q3Element.pos_j, Q3Element.neg_j,
74 Q3Element.pos_k, Q3Element.neg_k]
75
76/-- The spin-0 sector has 2 elements. -/
77theorem spin0_count : Spin0Sector.length = 2 := by decide
78
79/-- The spin-1 sector has 6 elements. -/
80theorem spin1_count : Spin1Sector.length = 6 := by decide
81
82/-- Q₃ has 8 elements total. -/
83theorem q3_order : Spin0Sector.length + Spin1Sector.length = 8 := by decide
84
85/-! ## Casimir Eigenvalues -/
86
87/-- Casimir eigenvalue for spin-j representation: C₂ = j(j+1). -/
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