pith. machine review for the scientific record. sign in
def definition def or abbrev

whyComplex

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 116def whyComplex : List String := [

proof body

Definition body.

 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/ℏ}. -/

depends on (21)

Lean names referenced from this declaration's body.