whyComplex

formal source

 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 -/
 124
 125/-- The Schrödinger equation: iℏ ∂ψ/∂t = Hψ
 126
 127    The i is essential! It ensures:
 128    1. Conservation of probability (unitarity)
 129    2. Wave-like solutions
 130    3. Interference
 131
 132    In RS: The i comes from the 8-tick generator.
 133    Time evolution = accumulating phase = multiplying by e^{-iEt/ℏ}. -/
 134theorem schrodinger_i_from_8tick :
 135    -- The i in Schrödinger equation is the 8-tick generator
 136    -- It ensures unitary (phase-preserving) evolution
 137    ∀ (ψ : ℝ → ℂ) (H : ℂ → ℂ) (ℏ : ℝ),
 138    (∀ t, ψ t = cexp (I * (-H (ψ t) * t / ℏ))) →
 139    ∃ (phase_gen : ℂ), phase_gen = I ∧ phase_gen = eightTickPhase 2 := by
 140  intro ψ H ℏ h_evol
 141  use I
 142  constructor
 143  · rfl
 144  · exact tick2_is_i.symm
 145
 146/-! ## Euler's Formula -/