`two`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.QFT.SpinStatistics on GitHub at line 76.

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

  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. -/
 101theorem int_half_exclusive (s : Spin) : ¬(s.isInteger ∧ s.isHalfInteger) := by
 102  unfold isInteger isHalfInteger
 103  omega
 104
 105end Spin
 106

papers checked against this theorem

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