phase_periodic

formal source

  29noncomputable def phase (k : Fin 8) : ℝ := (k : ℝ) * Real.pi / 4
  30
  31/-- The 8-tick phase is periodic with period 2π. -/
  32theorem phase_periodic : phase 0 + 2 * Real.pi = 2 * Real.pi := by
  33  unfold phase
  34  simp
  35
  36/-- Even ticks (0, 2, 4, 6) correspond to bosons. -/
  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