euler_from_8tick
plain-language theorem explainer
Euler's formula equates the complex exponential of iθ to cosine plus i sine for any real angle θ, grounding rotation in the 8-tick phase structure of Recognition Science. Quantum theorists and wave-equation modelers cite it to derive the appearance of i in the Schrödinger equation from tick-based rotations rather than postulate. The proof is a short tactic sequence that rewrites the exponential via the standard multiplication rule for i and simplifies algebraically.
Claim. For every real number θ, $e^{iθ} = cos θ + i sin θ$.
background
The Mathematics.ImaginaryUnit module derives i² = -1 from the 8-tick phase structure: rotation by two ticks (π/2) multiplies by i while four ticks (π) multiplies by -1, so i times i returns to -1. This supplies the generator for phase rotations that unify exponential growth or decay with trigonometric oscillation inside complex numbers. The local setting is MATH-001, which asks why imaginary numbers appear in physics and answers via the tick ladder that produces the imaginary unit as the π/2 rotator.
proof idea
The term-mode proof introduces the real parameter θ, rewrites cexp(I * θ) by the library lemma Complex.exp_mul_I, and closes with the ring tactic for algebraic simplification of the resulting cosine and sine terms.
why it matters
The declaration embeds Euler's formula inside the eight-tick octave (T7) of the forcing chain, explaining the i that appears in quantum mechanics and wave functions without external postulate. It supports the bridge from phase rotation to the mass formula and Berry threshold on the phi-ladder, and it directly precedes the sibling euler_identity that specializes to θ = π. No downstream uses are recorded, leaving open how the result propagates into the full Recognition Composition Law applications.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.