`value`

definition

show as: view math explainer →

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

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

  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
 107/-! ## 8-Tick Phase Accumulation -/
 108
 109/-- The phase accumulated by a spin-s particle over the 8-tick cycle.

papers checked against this theorem

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