euler_formula
plain-language theorem explainer
Euler's formula supplies the explicit map from real angles to the unit circle in the complex plane. Researchers deriving the necessity of complex numbers from Recognition Science's eight-tick ledger phases would cite it when representing rotations at multiples of 45 degrees. The proof is a one-line wrapper that commutes the factor of I and invokes the Mathlib identity Complex.exp_mul_I.
Claim. $e^{iθ} = cos θ + i sin θ$ for real θ.
background
The module MATH-004 derives the necessity of complex numbers from Recognition Science's 8-tick structure. The fundamental ledger cycle consists of eight phases, each a 45° rotation (360°/8). Rotations cannot be performed in one dimension, so the representation requires the plane; complex numbers encode exactly these 2D rotations via the exponential map. The phases are written e^{i π k /4} for k = 0 to 7, making Euler's formula the direct link between the exponential and trigonometric forms. The module states that this forces physics to employ ℂ because the ledger has phases.
proof idea
The proof rewrites the product I * θ to θ * I via mul_comm, then applies the library lemma Complex.exp_mul_I θ to obtain the cosine-plus-i-sine identity.
why it matters
This supplies the explicit identity required to embed the eight-tick phases into the complex plane, completing the core step of the module's argument that the ledger structure necessitates complex numbers. It directly supports the paper proposition outlined in the module doc-comment on Foundations of Physics. The result sits inside the T7 eight-tick octave landmark of the forcing chain and supplies the rotation representation used by sibling declarations on tick phases and phasors.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.