i_is_rotation

formal source

  72/-! ## Rotation and Multiplication -/
  73
  74/-- Multiplication by i is rotation by π/2 (2 ticks). -/
  75theorem i_is_rotation :
  76    ∀ z : ℂ, I * z = z * cexp (I * Real.pi / 2) := by
  77  intro z
  78  have h : cexp (I * Real.pi / 2) = I := by
  79    rw [Complex.exp_mul_I, Complex.cos_pi_div_two, Complex.sin_pi_div_two]
  80    simp
  81  rw [h, mul_comm]
  82
  83/-- Two rotations by π/2 equals rotation by π. -/
  84theorem two_rotations :
  85    cexp (I * Real.pi / 2) * cexp (I * Real.pi / 2) = cexp (I * Real.pi) := by
  86  rw [← Complex.exp_add]
  87  ring_nf
  88
  89/-- **THEOREM**: i² = -1 follows from 8-tick phase structure.
  90
  91    i = e^{iπ/2} (2 ticks from 1)
  92    i² = e^{iπ} = -1 (4 ticks from 1) -/
  93theorem i_squared_from_8tick :
  94    I^2 = -1 := by
  95  simp [sq, I_mul_I]
  96
  97/-- More generally: i^n corresponds to n×2 ticks. -/
  98theorem i_power_is_rotation (n : ℕ) :
  99    I^n = cexp (I * (n * Real.pi / 2)) := by
 100  have h : I = cexp (I * Real.pi / 2) := by
 101    rw [Complex.exp_mul_I, Complex.cos_pi_div_two, Complex.sin_pi_div_two]
 102    simp
 103  rw [h, ← Complex.exp_nat_mul]
 104  ring_nf
 105