phases_require_complex_k2
plain-language theorem explainer
The result shows that the phase for the second position in the eight-tick cycle has nonzero imaginary part. Researchers deriving the necessity of complex numbers from Recognition Science's ledger periodicity would cite this case. The tactic proof unfolds the phase map, reduces the argument via ring arithmetic, rewrites the exponential as cosine plus i times sine, and evaluates the sine at pi/2 to reach 1.
Claim. Let the phase at tick index $k$ be given by $e^{i k pi /4}$ for $k=0,1,2,3,4,5,6,7$. Then the imaginary part at $k=2$ satisfies $Im(e^{i pi/2}) = 1 ≠ 0$.
background
The module MATH-004 derives the necessity of complex numbers from the eight-tick phase structure of Recognition Science. The eight-tick phases are the angles $k pi /4$ for $k$ in Fin 8, supplied by the phase definition in Foundation.EightTick. The tick is the fundamental time quantum equal to 1 in RS-native units. tickPhase maps each index to the corresponding complex exponential on the unit circle. This k=2 instance is one of several concrete checks that rotations cannot be represented on the real line alone.
proof idea
The tactic proof unfolds tickPhase. It proves the auxiliary equality I * pi * 2 /4 = (pi/2) I by push_cast and ring. After specializing the Fin index to 2, it rewrites via exp_mul_I, replaces the exponential with ofReal cos and ofReal sin, simplifies the imaginary component, applies the identity sin(pi/2)=1, and closes with norm_num.
why it matters
The declaration supplies a concrete instance inside the MATH-004 derivation that eight-tick phases force complex numbers. It supports the parent claim that phases_require_complex and the broader necessity argument for quantum mechanics and electromagnetism. The result aligns with framework landmark T7 (eight-tick octave) by exhibiting the explicit 90-degree rotation that cannot live in one real dimension.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.