`zero`

definition

show as: view math explainer →

module: IndisputableMonolith.QFT.SpinStatistics
domain: QFT
line: 64 · 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 64.

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

formal source

  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 =>
  89  if h : s.twice % 2 = 1 then isTrue h else isFalse h
  90
  91/-- Decidable instance for integer check. -/
  92instance : DecidablePred isInteger := fun s =>
  93  if h : s.twice % 2 = 0 then isTrue h else isFalse h
  94

papers checked against this theorem

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