`ofInt`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.QFT.SpinStatistics on GitHub at line 58.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  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
  80
  81/-- Is this a half-integer spin (fermion)? -/
  82def isHalfInteger (s : Spin) : Prop := s.twice % 2 = 1
  83
  84/-- Is this an integer spin (boson)? -/
  85def isInteger (s : Spin) : Prop := s.twice % 2 = 0
  86
  87/-- Decidable instance for half-integer check. -/
  88instance : DecidablePred isHalfInteger := fun s =>

papers checked against this theorem

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