tick_phases_equally_spaced

formal source

  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
  85    ∃ (s : ℝ), x * y = s * x := by
  86  use y
  87  rw [mul_comm]
  88
  89/-- Complex multiplication includes rotation.
  90    z × w rotates z by arg(w) and scales by |w|. -/
  91theorem complex_rotation (z w : ℂ) :
  92    -- |z × w| = |z| × |w| (scaling)
  93    -- arg(z × w) = arg(z) + arg(w) modulo 2π (rotation) when both are nonzero
  94    ‖z * w‖ = ‖z‖ * ‖w‖ ∧
  95    (∀ hz : z ≠ 0, ∀ hw : w ≠ 0, (Complex.arg (z * w) : Real.Angle) = Complex.arg z + Complex.arg w) := by
  96  constructor
  97  · exact Complex.norm_mul z w