implications

formal source

 175    2. **Why waves oscillate**: Phase accumulation
 176    3. **Why QM is unitary**: Phase-preserving evolution
 177    4. **Why fermions get sign flip**: π rotation (4 ticks) = -1 -/
 178def implications : List String := [
 179  "i² = -1 from 4 ticks = π rotation",
 180  "Waves from continuous phase accumulation",
 181  "Unitarity from phase conservation",
 182  "Fermion sign from 2π rotation = 8 ticks = 1"
 183]
 184
 185/-! ## The 8th Roots of Unity -/
 186
 187/-- The 8th roots of unity ζ_k = e^{2πik/8} for k = 0,...,7.
 188
 189    These are exactly the 8-tick phases!
 190    They form a group under multiplication (cyclic group Z₈). -/
 191noncomputable def rootOfUnity (k : Fin 8) : ℂ :=
 192  cexp (I * (2 * Real.pi * k / 8))
 193
 194/-- The roots form a group. -/
 195theorem roots_form_group :
 196    ∀ j k : Fin 8, rootOfUnity j * rootOfUnity k = rootOfUnity (j + k) := by
 197  intro j k
 198  unfold rootOfUnity
 199  rw [← Complex.exp_add]
 200  push_cast
 201  have h_val : ((j + k : Fin 8).val : ℝ) = ((j.val + k.val) % 8 : ℕ) := by
 202    simp only [Fin.val_add]
 203  rw [h_val]
 204  have h_div : (j.val + k.val : ℕ) = ((j.val + k.val) % 8) + 8 * ((j.val + k.val) / 8) := by
 205    rw [add_comm, Nat.div_add_mod]
 206  push_cast
 207  rw [h_div]
 208  rw [mul_add, add_div, mul_add]