euler_formula
plain-language theorem explainer
Euler's formula supplies the explicit map from real angle to complex rotation via the exponential. Recognition Science researchers modeling 8-tick ledger phases as roots of unity would cite it to justify the complex plane. The proof is a one-line wrapper that commutes the scalar multiplication and applies the standard library identity for exp(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 phase structure. The ledger cycle produces eight equally spaced phases at multiples of π/4; each phase is a rotation, which cannot be represented in one real dimension and therefore requires the two-dimensional algebra of the complex plane. The supplied module doc states that the phases are represented by e^{i π k /4} and concludes that physics must therefore employ ℂ.
proof idea
Term-mode proof. The single rewrite commutes I and θ; the exact step invokes the library lemma Complex.exp_mul_I θ.
why it matters
The declaration supplies the algebraic identity needed to represent the eight-tick phases inside the complex plane, directly supporting the module's core claim that the ledger structure forces complex numbers (T7 eight-tick octave). No parent theorems appear in the used-by graph. It closes the local derivation from phase rotations to ℂ without introducing new axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.