phases_require_complex_k1
plain-language theorem explainer
The theorem shows that the imaginary part of the complex phase at the first tick in the eight-tick cycle is nonzero. Researchers deriving the necessity of complex numbers for quantum mechanics or phasors from an eight-tick ledger would cite this. The proof unfolds the phase definition, reduces the argument via ring simplification, applies the exponential formula, and invokes positivity of sin(π/4).
Claim. Let the eight-tick phase at step $k$ be represented by the complex exponential $e^{i k π / 4}$. Then the imaginary part of the representation at $k=1$ satisfies $Im(e^{i π / 4}) ≠ 0$.
background
The module MATH-004 derives the necessity of complex numbers from Recognition Science's eight-tick phase structure. The phases are the angles $kπ/4$ for $k=0..7$, lifted to complex exponentials $e^{i k π /4}$ because rotations cannot be represented in one real dimension. Upstream, EightTick.phase supplies the real-valued angle definition $(k:ℝ)·π/4$, while tickPhase in the same module supplies the complex lift used here.
proof idea
The tactic proof unfolds tickPhase, rewrites the multiplier $I·π·1/4$ to $(π/4)·I$ by ring, substitutes the Fin 8 value, applies Complex.exp_mul_I and the cos/sin decomposition, extracts the imaginary component, replaces it by Real.sin_pi_div_four, and closes with positivity.
why it matters
This fills the first concrete step in the module's derivation that the eight-tick octave (T7) forces complex numbers for phase representation. It supports the parent claim that physics requires ℂ because the ledger cycle contains rotations, and precedes the sibling results phases_require_complex_k2 and phases_require_complex. It directly instantiates the module insight that rotation in the plane is the origin of the imaginary unit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.