`Spin`

definition

show as: view math explainer →

module: IndisputableMonolith.QFT.SpinStatistics
domain: QFT
line: 49 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.QFT.SpinStatistics on GitHub at line 49.

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

depends on

used by

formal source

  46/-! ## Spin Representation -/
  47
  48/-- Spin quantum number as a half-integer (n/2 for integer n). -/
  49structure Spin where
  50  /-- Twice the spin value (to keep integer arithmetic). -/
  51  twice : ℤ
  52  /-- Spin must be non-negative. -/
  53  nonneg : twice ≥ 0
  54
  55namespace Spin
  56
  57/-- Create a spin from an integer (s = n means spin n). -/
  58def ofInt (n : ℕ) : Spin := ⟨2 * n, by omega⟩
  59
  60/-- Create a half-integer spin (s = n/2). -/
  61def halfInt (n : ℕ) : Spin := ⟨n, by omega⟩
  62
  63/-- Spin 0. -/
  64def zero : Spin := ofInt 0
  65
  66/-- Spin 1/2 (electron, quarks). -/
  67def half : Spin := halfInt 1
  68
  69/-- Spin 1 (photon, W/Z, gluon). -/
  70def one : Spin := ofInt 1
  71
  72/-- Spin 3/2 (hypothetical gravitino). -/
  73def threeHalves : Spin := halfInt 3
  74
  75/-- Spin 2 (graviton). -/
  76def two : Spin := ofInt 2
  77
  78/-- The actual spin value as a real number. -/
  79noncomputable def value (s : Spin) : ℝ := s.twice / 2

papers checked against this theorem

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