`one`

definition

show as: view math explainer →

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

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

  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
  95/-- Spin is either integer or half-integer. -/
  96theorem int_or_half (s : Spin) : s.isInteger ∨ s.isHalfInteger := by
  97  unfold isInteger isHalfInteger
  98  omega
  99
 100/-- Integer and half-integer are mutually exclusive. -/

papers checked against this theorem

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