phases_require_complex_k1
The first non-trivial phase in the eight-tick cycle has nonzero imaginary part when expressed via complex exponential. Foundational physicists deriving the origin of complex numbers in quantum mechanics or electromagnetism from Recognition Science structures would cite this result. The proof unfolds the phase map, reduces the argument via ring rewriting, invokes the Euler identity to isolate the sine term, and confirms positivity of sin(π/4).
claim$Im(e^{iπ/4}) ≠ 0$, where the exponential represents the phase factor at the first position in the eight-tick cycle.
background
The module MATH-004 shows that complex numbers arise because the Recognition Science ledger possesses an eight-tick cycle whose phases are rotations. Upstream, the EightTick.phase definition supplies the real angle kπ/4 for k in Fin 8. The tickPhase map converts each angle into the corresponding complex exponential e^{iθ}. This theorem supplies the first concrete witness that the rotation cannot be captured inside the reals alone.
proof idea
The tactic proof unfolds tickPhase, rewrites the multiplier I·π·1/4 to (π/4)·I via push_cast and ring, applies the identity exp(iθ) = cos θ + i sin θ, extracts the imaginary part, substitutes the known value sin(π/4) = √2/2, and concludes by positivity.
why it matters in Recognition Science
The result occupies the opening concrete step in the MATH-004 derivation that eight-tick phases force two-dimensional rotations and therefore the complex plane (T7 eight-tick octave). It directly supports the subsequent claims phases_require_complex_k2 and quantum_requires_complex. The argument closes one link in the chain from the primitive ledger cycle to the appearance of i in physical equations.
scope and limits
- Does not establish the claim for every tick index simultaneously.
- Does not derive the eight-tick structure from more primitive axioms.
- Does not supply an empirical test or measurement protocol.
- Does not address whether alternative number systems could represent the same phases.
formal statement (Lean)
104theorem phases_require_complex_k1 : (tickPhase ⟨1, by omega⟩).im ≠ 0 := by
proof body
Tactic-mode proof.
105 unfold tickPhase
106 -- exp(I * π / 4) = cos(π/4) + I * sin(π/4)
107 have h : I * ↑π * ↑(1 : ℕ) / 4 = ↑(π / 4 : ℝ) * I := by push_cast; ring
108 simp only [show (⟨1, by omega⟩ : Fin 8).val = 1 from rfl] at *
109 rw [h, Complex.exp_mul_I]
110 rw [← Complex.ofReal_cos, ← Complex.ofReal_sin]
111 simp only [Complex.add_im, Complex.mul_I_im, Complex.ofReal_im, Complex.ofReal_re, zero_add]
112 -- sin(π/4) = √2/2 ≠ 0
113 rw [Real.sin_pi_div_four]
114 exact ne_of_gt (by positivity)
115
116/-- The phase at k=2 (which is π/2) also has nonzero imaginary part. -/