phasor
The phasor definition supplies the standard complex representation of a sinusoidal signal with real amplitude and phase. Physicists analyzing AC circuits or electromagnetic waves cite it to move between time-domain cosine forms and frequency-domain exponentials. It is a direct one-line wrapper that multiplies the amplitude by the complex exponential of the supplied phase angle.
claimFor real amplitude $A$ and phase angle $φ$, the phasor is the complex number $A e^{i φ}$.
background
The module MATH-004 derives the necessity of complex numbers from Recognition Science's 8-tick phase structure. The 8-tick cycle consists of phases $kπ/4$ for $k=0$ to $7$, each a 45° rotation; such rotations cannot be represented in one real dimension and therefore require the plane of complex numbers. Upstream, the EightTick.phase definition supplies the discrete phases $kπ/4$, while the Wedge.phase definition supplies the general unimodular complex exponential $e^{i w}$.
proof idea
One-line wrapper that multiplies the real amplitude by Complex.exp of (I times the real phase), using the standard embedding of the exponential map into ℂ.
why it matters in Recognition Science
This definition fills the electromagnetism slot in the module's argument that the 8-tick octave (T7) forces complex numbers for any physical rotation or oscillation. It supports the broader claim that physics requires ℂ because the ledger phases are rotations, linking directly to the module's target of showing why wavefunctions, phasors, and Fourier transforms are complex. No downstream theorems are listed yet.
scope and limits
- Does not prove that complex numbers are required by the 8-tick structure.
- Does not restrict the phase input to multiples of π/4.
- Does not embed time dependence or frequency into the definition.
- Does not derive the equivalence between the exponential and cosine forms.
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 -/