tick2_is_i
plain-language theorem explainer
This result identifies the imaginary unit with the phase advance after two ticks in the eight-tick cycle. Quantum theorists deriving complex structure from discrete time would cite it to ground the i in the Schrödinger equation. The proof unfolds the phase map, reduces the argument to π/2 via ring simplification, and evaluates the complex exponential using standard cosine and sine values at that angle.
Claim. The phase rotation after two ticks in the eight-tick cycle equals the imaginary unit: the factor for index 2 satisfies $e^{i π/2} = i$.
background
The module MATH-001 derives the imaginary unit from the eight-tick phase rotation in Recognition Science. Ticks are discrete atomic units of time (Fin 8) with no background manifold; the phase map sends tick index k to exp(I * 2π k / 8), so that two ticks advance the phase by π/2 and yield i. This matches the module statement that rotation by 2 ticks (π/2) corresponds to multiplication by i.
proof idea
The proof unfolds eightTickPhase, simplifies the Fin 2 value and natural-number cast, rewrites the multiplier via ring to I * (π/2), applies the complex exponential identity exp(I θ) = cos θ + I sin θ, substitutes the known values cos(π/2) = 0 and sin(π/2) = 1, and finishes with simp.
why it matters
This supplies the identification used by the downstream theorem schrodinger_i_from_8tick, which shows the i in the Schrödinger equation arises as the eight-tick phase generator ensuring unitary evolution. It completes the MATH-001 target of grounding i² = -1 in the RS eight-tick structure and links directly to the T7 eight-tick octave in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.