cyclePhase

formal source

 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) :
 127    cyclePhase s = -1 := by
 128  unfold cyclePhase Spin.value Spin.isHalfInteger at *
 129  -- s.twice is odd, so s.twice % 2 = 1
 130  have hodd : s.twice % 2 = 1 := h
 131  -- Get k such that s.twice = 2k + 1
 132  have ⟨k, hk⟩ := Int.odd_iff.mpr hodd
 133  -- The phase is exp(2πi × (twice/2)) = exp(πi × twice)
 134  have h_rewrite : 2 * π * I * (s.twice / 2 : ℝ) = π * I * s.twice := by
 135    push_cast; ring
 136  rw [h_rewrite, hk]
 137  push_cast
 138  -- exp(πi × (2k+1)) = exp(2kπi) × exp(πi) = 1 × (-1) = -1
 139  have h_split : π * I * (2 * k + 1) = (k : ℂ) * (2 * π * I) + π * I := by ring
 140  rw [h_split, Complex.exp_add, Complex.exp_int_mul_two_pi_mul_I, one_mul, Complex.exp_pi_mul_I]
 141