tickPhase

formal source

  47/-! ## The 8-Tick Phase Structure -/
  48
  49/-- The 8 phases of the recognition tick cycle. -/
  50noncomputable def tickPhase (k : Fin 8) : ℂ :=
  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.