i_squared_from_8tick

formal source

  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
 115    In RS, all of these trace back to the 8-tick phase structure! -/
 116def whyComplex : List String := [
 117  "Waves: sin(θ) = Im(e^{iθ})",
 118  "Quantum: States are complex, |ψ|² = probability",
 119  "Rotations: e^{iθ} rotates by θ",
 120  "Fourier: f(x) = ∫ F(k) e^{ikx} dk"
 121]
 122
 123/-! ## The Schrödinger Equation -/