pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Mathematics.ImaginaryUnit

show as:
view Lean formalization →

The module maps the discrete 8-tick cycle onto the unit circle in the complex plane, showing how the imaginary unit arises at the second tick. Researchers deriving quantum evolution or rotation operators from discrete time foundations would cite these constructions. The module proceeds by defining a phase assignment function and verifying its algebraic closure after eight steps.

claimThe eight-tick phases are the points $e^{i k π/4}$ for integer $k=0$ to $7$ on the unit circle, with the imaginary unit $i$ realized at tick 2 as $e^{i π/2}$.

background

Recognition Science takes the fundamental time quantum τ₀ = 1 tick from the Constants module. The EightTick module supplies the discrete clock whose phases sit at multiples of π/4: 0, π/4, π/2, 3π/4, π, 5π/4, 3π/2, 7π/4. This module translates those ticks into complex numbers via a phase map that places each tick at the corresponding point on the unit circle.

proof idea

This is a definition module, no proofs. It introduces the phase assignment, then records a chain of lemmas that compute the explicit values at each tick and confirm the cycle returns to 1 after eight steps.

why it matters in Recognition Science

The module supplies the link from the eight-tick octave (T7) to the complex plane, enabling later results on the Schrödinger equation and Euler identity inside the same module. It thereby converts the discrete clock into the algebraic structure needed for rotation operators and phase evolution.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (15)