int_or_half

formal source

  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)
 113
 114/-- The phase accumulated over half an 8-tick cycle (4 ticks = π rotation). -/
 115noncomputable def halfCyclePhase (s : Spin) : ℂ :=
 116  Complex.exp (π * I * s.value)
 117
 118/-- The exchange phase: phase under particle exchange.
 119    In QFT, exchanging two identical particles is equivalent to a 2π rotation. -/
 120noncomputable def exchangePhase (s : Spin) : ℂ := cyclePhase s
 121
 122/-! ## The Spin-Statistics Connection -/
 123
 124/-- **THEOREM (Fermion Phase)**: Half-integer spin particles acquire a minus sign
 125    under the full 8-tick cycle (2π rotation). -/
 126theorem fermion_antisymmetric (s : Spin) (h : s.isHalfInteger) :