euler_formula
plain-language theorem explainer
Euler's formula equates the complex exponential of an imaginary argument to the sum of cosine and i times sine. Workers on the 8-tick phase cycles in Recognition Science cite it to justify representing ledger rotations in the complex plane. The proof is a term-mode reduction that commutes the multiplication and applies the library identity Complex.exp_mul_I.
Claim. For every real number $θ$, $e^{iθ} = cos θ + i sin θ$.
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 at 45-degree intervals, each a rotation that cannot be realized in one dimension and therefore requires the two-dimensional plane encoded by ℂ. The supplied upstream results record auxiliary structures such as spectral-peak classification and collision-free programs that presuppose the same phase representation.
proof idea
The term proof first rewrites the product to place the imaginary unit on the left, then applies the exact library lemma Complex.exp_mul_I θ.
why it matters
The declaration supplies the explicit bridge between exponential and trigonometric forms required by the 8-tick octave (T7) in the forcing chain. It directly supports sibling developments such as the Schrödinger equation and phasor constructions listed in the module. The module documentation positions it as the central step in the MATH-004 argument that physics must adopt ℂ because the ledger phases are rotations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.