euler_formula
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not derive the 8-tick cycle or its period 2^3.
- Does not compare ℂ to quaternions or other division algebras.
- Does not connect to the J-cost function or phi-ladder mass formulas.
- Does not address the alpha band or Berry threshold.
formal statement (Lean)
203theorem euler_formula (θ : ℝ) :
204 Complex.exp (I * θ) = Complex.cos θ + Complex.sin θ * I := by
proof body
Term-mode proof.
205 rw [mul_comm]
206 exact Complex.exp_mul_I θ
207
208/-! ## Alternative Number Systems -/
209
210/-- Could we use quaternions (ℍ) instead?
211 ℍ has 3 imaginary units: i, j, k
212 This is "too much" - ℂ is just right for 2D rotation. -/