phasor
The phasor definition maps a real amplitude and phase to the complex number amplitude times exp(i times phase). Electromagnetism and signal-processing researchers cite it to replace trigonometric AC expressions with complex exponentials. It sits inside the module deriving complex-number necessity from the eight-tick phase rotations of Recognition Science. The implementation is a direct one-line wrapper around the standard complex exponential.
claimThe phasor with real amplitude $A$ and phase $φ$ equals $A exp(i φ)$.
background
The module MATH-004 derives the necessity of complex numbers from Recognition Science's eight-tick phase structure. Upstream, EightTick.phase supplies the discrete phases $k π / 4$ for $k = 0,…,7$, while Wedge.phase supplies the unimodular complex number $exp(i w)$. These phases are rotations that cannot be represented in one real dimension, forcing the use of the complex plane. The supplied doc-comment notes the electromagnetism application: $V(t) = V_0 cos(ωt + φ)$ corresponds to the complex form $V_0 exp(i(ωt + φ))$.
proof idea
This definition is a one-line wrapper that multiplies the real amplitude by the complex exponential of i times the supplied phase.
why it matters in Recognition Science
The definition supplies the concrete phasor representation required by the module's argument that eight-tick rotations (T7) force complex numbers into physics. It directly supports the claim that the ledger's phase structure cannot be captured in the reals alone. No downstream theorems are listed, yet the definition underpins the complex amplitudes appearing in S-matrix and double-slit contexts within the same framework.
scope and limits
- Does not prove that complex numbers are required by physics.
- Does not enumerate the eight discrete tick phases.
- Does not relate the phasor to the Recognition Composition Law.
- Does not connect amplitude or phase to the phi-ladder or mass formula.
formal statement (Lean)
176noncomputable def phasor (amplitude phase : ℝ) : ℂ :=
proof body
Definition body.
177 amplitude * Complex.exp (I * phase)
178
179/-- Fourier transform: Decomposes functions into complex exponentials.
180 F(ω) = ∫ f(t) e^{-iωt} dt -/