whyComplex
plain-language theorem explainer
This definition supplies a four-item list that motivates the appearance of complex numbers in physics by tracing each use to the 8-tick phase generator. Foundational physicists working inside Recognition Science cite it when they need a compact statement of why i enters wave equations, quantum states, rotations, and Fourier transforms. The entry is supplied verbatim as a constant list with no computation or lemmas.
Claim. Complex numbers are required because waves satisfy $sin(θ) = Im(e^{iθ})$, quantum states are complex vectors whose squared modulus gives probability, multiplication by $e^{iθ}$ encodes planar rotations, and Fourier integrals decompose functions via $e^{ikx}$. Recognition Science derives all four from the eight-tick phase structure whose generator produces $i$ after two ticks.
background
The module MATH-001 sets out to obtain $i^2 = -1$ from the eight-tick phase rotation. Its central object is the phase map that assigns to each tick index $k$ in Fin 8 the angle $kπ/4$. The upstream constant tick supplies the fundamental time quantum $τ_0 = 1$ in RS-native units, while EightTick.phase states that these phases are periodic with period $2π$. Constants.RSNativeUnits.Time simply aliases the reals so that time and phase live in the same field.
proof idea
Direct definition that returns the fixed list of four explanatory strings; no tactics or upstream lemmas are invoked inside the body.
why it matters
The entry supplies the physical motivation that precedes the formal siblings tick2_is_i and i_squared_from_8tick. It therefore anchors the claim that the imaginary unit is the generator of the eight-tick octave (T7) and explains the presence of $i$ in the Schrödinger equation via phase accumulation. No downstream theorems yet consume the list, leaving open the question of how to embed these explanatory strings into a single formal statement of the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.