reals_no_rotation

formal source

  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
  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