phases_require_complex_k2
plain-language theorem explainer
The phase factor at the second position in the 8-tick cycle equals e^{i π/2} and therefore carries a nonzero imaginary part. Researchers deriving quantum mechanics or signal processing from discrete periodic structures cite this to show that 90-degree rotations cannot stay inside the reals. The proof unfolds the phase definition, reduces the argument to π/2 by ring arithmetic and casting, then invokes the sine value at that point to exhibit the imaginary unit explicitly.
Claim. Let $e^{i k π /4}$ denote the phase factor for tick index $k$ in the fundamental 8-tick cycle. Then the imaginary part of the factor at $k=2$ satisfies $e^{i π /2} = i$, so its imaginary component is nonzero.
background
The module MATH-004 shows that the Recognition Science 8-tick octave forces complex numbers because each tick advances the ledger by a 45-degree rotation. The upstream phase definition supplies the real angle $k π /4$ for $k$ in Fin 8, while tick supplies the unit time step. tickPhase wraps this angle inside the complex exponential $e^{i θ_k}$ so that the full cycle lives in the plane rather than on the line.
proof idea
Unfold tickPhase to expose the exponential. Establish the algebraic identity I * π * 2 / 4 = (π/2) I by push_cast and ring. Rewrite via exp_mul_I and the real/imaginary projections of cos and sin. Apply the known value sin(π/2) = 1 together with norm_num to obtain imaginary part exactly 1.
why it matters
The result supplies one concrete case inside the general argument that the eight-tick octave (T7) cannot be represented without the imaginary unit. It feeds the sibling claim phases_require_complex and ultimately the derivation that quantum wavefunctions and phasors must be complex. The module doc-comment frames this as the foundational reason physics employs ℂ rather than ℝ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.