tick4_is_neg1
Tick 4 in the eight-tick phase cycle equals negative one on the complex unit circle. Researchers deriving the imaginary unit from discrete rotation structures in Recognition Science cite this as a direct verification of the four-tick half-cycle. The proof unfolds the phase definition, reduces the argument via ring arithmetic, and substitutes the known cosine and sine values at pi.
claimIn the eight-tick phase cycle given by $e^{i n pi / 4}$ for integer $n$ modulo 8, the phase at tick 4 satisfies $e^{i pi} = -1$.
background
The module MATH-001 derives i squared equals negative one from the eight-tick phase structure of Recognition Science. The eight-tick phase at step n is defined by the complex exponential cexp(I times (n times pi divided by 4)), placing tick 0 at 1, tick 2 at i, tick 4 at negative one, and tick 6 at negative i. This construction supplies the generator of quarter-turn rotations that later yields the imaginary unit in the Schrödinger equation and Euler's formula.
proof idea
The tactic proof unfolds eightTickPhase, simplifies the Fin 4 argument to 4 times pi over 4, introduces a ring equality reducing the multiplier to I times pi, rewrites via Complex.exp_mul_I, substitutes Complex.cos_pi and Complex.sin_pi, and finishes with simp to reach negative one.
why it matters in Recognition Science
The result supplies the explicit four-tick half-cycle inside the eight-tick octave (T7) that forces complex arithmetic in the Recognition framework. It directly supports the sibling derivations of i squared from eight ticks and the Euler identity in the same module, confirming why the imaginary unit appears in quantum wave equations. The step closes one concrete link between the discrete phase ladder and standard complex analysis without additional hypotheses.
scope and limits
- Does not compute phases for ticks other than 4.
- Does not derive the value of i itself.
- Does not connect the phase to any physical observable or measurement.
- Does not address rotations outside the unit circle.
formal statement (Lean)
64theorem tick4_is_neg1 : eightTickPhase 4 = -1 := by
proof body
Tactic-mode proof.
65 unfold eightTickPhase
66 simp only [Fin.val_four, Nat.cast_ofNat]
67 have h : I * (4 * Real.pi / 4) = I * Real.pi := by ring
68 rw [h]
69 rw [Complex.exp_mul_I, Complex.cos_pi, Complex.sin_pi]
70 simp
71
72/-! ## Rotation and Multiplication -/
73
74/-- Multiplication by i is rotation by π/2 (2 ticks). -/