complex_rotation

formal source

  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
  98  · intro hz hw
  99    -- Use arg_mul_coe_angle which works modulo 2π
 100    exact Complex.arg_mul_coe_angle hz hw
 101
 102/-- **THEOREM**: 8-tick phases require rotation, which requires ℂ.
 103    The first non-trivial phase (k=1) has nonzero imaginary part. -/
 104theorem phases_require_complex_k1 : (tickPhase ⟨1, by omega⟩).im ≠ 0 := by
 105  unfold tickPhase
 106  -- exp(I * π / 4) = cos(π/4) + I * sin(π/4)
 107  have h : I * ↑π * ↑(1 : ℕ) / 4 = ↑(π / 4 : ℝ) * I := by push_cast; ring
 108  simp only [show (⟨1, by omega⟩ : Fin 8).val = 1 from rfl] at *
 109  rw [h, Complex.exp_mul_I]
 110  rw [← Complex.ofReal_cos, ← Complex.ofReal_sin]
 111  simp only [Complex.add_im, Complex.mul_I_im, Complex.ofReal_im, Complex.ofReal_re, zero_add]
 112  -- sin(π/4) = √2/2 ≠ 0
 113  rw [Real.sin_pi_div_four]
 114  exact ne_of_gt (by positivity)
 115
 116/-- The phase at k=2 (which is π/2) also has nonzero imaginary part. -/
 117theorem phases_require_complex_k2 : (tickPhase ⟨2, by omega⟩).im ≠ 0 := by
 118  unfold tickPhase
 119  have h : I * ↑π * ↑(2 : ℕ) / 4 = ↑(π / 2 : ℝ) * I := by push_cast; ring
 120  simp only [show (⟨2, by omega⟩ : Fin 8).val = 2 from rfl] at *
 121  rw [h, Complex.exp_mul_I]