two_rotations

formal source

  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
 106/-! ## Why Physics Needs Complex Numbers -/
 107
 108/-- Complex numbers are necessary in physics because:
 109
 110    1. **Waves**: Sinusoidal waves are Re(e^{iωt})
 111    2. **Quantum mechanics**: States are complex vectors
 112    3. **Rotations**: Complex numbers encode 2D rotations
 113    4. **Fourier analysis**: Frequency decomposition uses e^{ikx}
 114