isHalfInteger

formal source

  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.
 110    For a 2π rotation (one complete cycle), the phase is exp(2πis). -/
 111noncomputable def cyclePhase (s : Spin) : ℂ :=
 112  Complex.exp (2 * π * I * s.value)