tick4_is_neg1
plain-language theorem explainer
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.
Claim. In 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.