isOddTick

formal source

  37def isEvenTick (k : Fin 8) : Bool := k.val % 2 = 0
  38
  39/-- Odd ticks (1, 3, 5, 7) correspond to fermions. -/
  40def isOddTick (k : Fin 8) : Bool := k.val % 2 = 1
  41
  42/-- Phase advance by one tick. -/
  43noncomputable def nextPhase (k : Fin 8) : Fin 8 := ⟨(k.val + 1) % 8, Nat.mod_lt _ (by norm_num)⟩
  44
  45/-- The complex exponential of a phase. -/
  46noncomputable def phaseExp (k : Fin 8) : ℂ := Complex.exp (Complex.I * phase k)
  47
  48/-- **THEOREM**: The 8th power of each phase gives 1.
  49    exp(i × k × π/4)^8 = exp(2πik) = 1.
  50    Uses periodicity: exp(2πin) = 1 for n ∈ ℤ. -/
  51theorem phase_eighth_power_is_one (k : Fin 8) :
  52    (phaseExp k)^8 = 1 := by
  53  unfold phaseExp phase
  54  rw [← Complex.exp_nat_mul]
  55  -- 8 * (I * (k * π / 4)) = 2kπI, and exp(2kπI) = 1
  56  have h : (8 : ℕ) * (Complex.I * ((k.val : ℕ) * Real.pi / 4 : ℝ)) = 2 * Real.pi * Complex.I * k.val := by
  57    push_cast
  58    ring
  59  simp only [] at h
  60  rw [show (k : ℕ) = k.val from rfl] at h ⊢
  61  convert Complex.exp_int_mul_two_pi_mul_I k.val using 2
  62  push_cast
  63  ring
  64
  65/-- Phase at k=4 gives -1 (fermion phase).
  66    This is the key to antisymmetry under particle exchange. -/
  67theorem phase_4_is_minus_one : phaseExp ⟨4, by norm_num⟩ = -1 := by
  68  unfold phaseExp phase
  69  have h : Complex.I * ((4 : ℕ) * Real.pi / 4 : ℝ) = Real.pi * Complex.I := by
  70    push_cast