tick_phases_roots_of_unity

formal source

  51  Complex.exp (I * π * k / 4)
  52
  53/-- **THEOREM**: The 8 tick phases are 8th roots of unity. -/
  54theorem tick_phases_roots_of_unity (k : Fin 8) :
  55    (tickPhase k)^8 = 1 := by
  56  unfold tickPhase
  57  -- exp(I × π × k / 4)^8 = exp(8 × I × π × k / 4) = exp(2πIk) = 1
  58  rw [← Complex.exp_nat_mul]
  59  have h : (8 : ℕ) * (I * ↑π * ↑(k : ℕ) / 4) = ↑(k : ℕ) * (2 * ↑π * I) := by
  60    push_cast
  61    ring
  62  rw [h]
  63  exact Complex.exp_nat_mul_two_pi_mul_I k
  64
  65/-- The phases are equally spaced around the unit circle.
  66    Consecutive phases differ by π/4 (45°). -/
  67theorem tick_phases_equally_spaced (j k : Fin 8) (hjk : j < k) :
  68    -- The quotient tickPhase k / tickPhase j has argument (k - j) * π/4 modulo 2π
  69    tickPhase k / tickPhase j = Complex.exp ((k.val - j.val : ℝ) * π / 4 * I) := by
  70  unfold tickPhase
  71  -- Use exp_sub: exp(a) / exp(b) = exp(a - b)
  72  rw [← Complex.exp_sub]
  73  congr 1
  74  -- Show: I * π * k / 4 - I * π * j / 4 = (k - j) * π / 4 * I
  75  push_cast
  76  ring
  77
  78/-! ## Why Real Numbers Are Insufficient -/
  79
  80/-- The problem with real numbers: they can't represent rotation.
  81    In ℝ, multiplication is just scaling. No rotation. -/
  82theorem reals_no_rotation (x y : ℝ) (hx : x ≠ 0) (hy : y ≠ 0) :
  83    -- In ℝ: x × y is on the same line as x and y
  84    -- No perpendicular component