euler_identity

formal source

 163
 164    Often called "the most beautiful equation."
 165    In RS, it says: 4 ticks around the circle returns to -1. -/
 166theorem euler_identity : cexp (I * Real.pi) + 1 = 0 := by
 167  rw [Complex.exp_mul_I, Complex.cos_pi, Complex.sin_pi]
 168  simp
 169
 170/-! ## Deep Implications -/
 171
 172/-- The 8-tick structure explains:
 173
 174    1. **Why i² = -1**: Half-way around the phase circle
 175    2. **Why waves oscillate**: Phase accumulation
 176    3. **Why QM is unitary**: Phase-preserving evolution
 177    4. **Why fermions get sign flip**: π rotation (4 ticks) = -1 -/
 178def implications : List String := [
 179  "i² = -1 from 4 ticks = π rotation",
 180  "Waves from continuous phase accumulation",
 181  "Unitarity from phase conservation",
 182  "Fermion sign from 2π rotation = 8 ticks = 1"
 183]
 184
 185/-! ## The 8th Roots of Unity -/
 186
 187/-- The 8th roots of unity ζ_k = e^{2πik/8} for k = 0,...,7.
 188
 189    These are exactly the 8-tick phases!
 190    They form a group under multiplication (cyclic group Z₈). -/
 191noncomputable def rootOfUnity (k : Fin 8) : ℂ :=
 192  cexp (I * (2 * Real.pi * k / 8))
 193
 194/-- The roots form a group. -/
 195theorem roots_form_group :
 196    ∀ j k : Fin 8, rootOfUnity j * rootOfUnity k = rootOfUnity (j + k) := by