phases_require_complex_k2
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.
claimLet $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 in Recognition Science
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 ℝ.
scope and limits
- Does not prove the nonzero-imaginary claim for the remaining six indices.
- Does not derive the full field structure of the complexes from the phases.
- Does not link the phase factor to any physical observable or measurement.
- Does not address whether the same necessity arises in continuous time.
formal statement (Lean)
117theorem phases_require_complex_k2 : (tickPhase ⟨2, by omega⟩).im ≠ 0 := by
proof body
Tactic-mode proof.
118 unfold tickPhase
119 have h : I * ↑π * ↑(2 : ℕ) / 4 = ↑(π / 2 : ℝ) * I := by push_cast; ring
120 simp only [show (⟨2, by omega⟩ : Fin 8).val = 2 from rfl] at *
121 rw [h, Complex.exp_mul_I]
122 rw [← Complex.ofReal_cos, ← Complex.ofReal_sin]
123 simp only [Complex.add_im, Complex.mul_I_im, Complex.ofReal_im, Complex.ofReal_re, zero_add]
124 rw [Real.sin_pi_div_two]
125 norm_num
126
127/-- General statement: for k ∈ {1,2,3,5,6,7}, the tick phase has nonzero imaginary part. -/