phasor
plain-language theorem explainer
Phasor expresses a real amplitude and phase as the complex number given by amplitude times the exponential of i times phase. Electromagnetism and signal-processing researchers cite it when converting between trigonometric and exponential forms for AC analysis. The definition is a direct one-line abbreviation of the Euler representation.
Claim. For real amplitude $A$ and phase $φ$, the phasor is $A e^{i φ}$.
background
The module derives the necessity of complex numbers from Recognition Science's 8-tick phase structure, where each tick is a 45° rotation and rotations require a two-dimensional plane. Upstream, the EightTick.phase definition supplies the eight phases $kπ/4$ for $k=0..7$, while the Wedge.phase definition supplies the unimodular complex exponential $e^{i w}$. The supplied doc-comment states that phasors simplify AC analysis via the correspondence $V(t)=V_0 cos(ωt+φ) ↔ V_0 e^{i(ωt+φ)}$.
proof idea
One-line definition that multiplies the supplied real amplitude by Complex.exp of (I times the supplied phase).
why it matters
The definition supplies the concrete representation needed to embed 8-tick phases into electromagnetism and quantum mechanics inside the MATH-004 argument. It fills the module's target of showing that the ledger's eight phases force the use of ℂ because rotations cannot be performed in one dimension. No downstream theorems are recorded yet; the module doc-comment points to a prospective paper on foundations of physics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.