phaseExp

formal source

  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
  71    ring
  72  rw [h, Complex.exp_pi_mul_I]
  73
  74/-- Phase at k=0 gives 1 (boson phase).
  75    This is the identity phase - no change under exchange. -/
  76theorem phase_0_is_one : phaseExp ⟨0, by norm_num⟩ = 1 := by