`Q3Element`

definition

show as: view math explainer →

module: IndisputableMonolith.StandardModel.Q3Representations
domain: StandardModel
line: 56 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.StandardModel.Q3Representations on GitHub at line 56.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

used by

formal source

  53/-! ## Q₃ Group Structure -/
  54
  55/-- The 8 elements of the quaternion group Q₃ = {±1, ±i, ±j, ±k}. -/
  56inductive Q3Element
  57  | pos_one  : Q3Element  -- +1
  58  | neg_one  : Q3Element  -- -1
  59  | pos_i    : Q3Element  -- +i
  60  | neg_i    : Q3Element  -- -i
  61  | pos_j    : Q3Element  -- +j
  62  | neg_j    : Q3Element  -- -j
  63  | pos_k    : Q3Element  -- +k
  64  | neg_k    : Q3Element  -- -k
  65  deriving DecidableEq, Repr
  66
  67/-- The spin-0 sector (scalar sector): {+1, -1}. These are the Higgs generators. -/
  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.