pith. sign in
module module high

IndisputableMonolith.Mathematics.ImaginaryUnit

show as:
view Lean formalization →

The Mathematics.ImaginaryUnit module maps the 8-tick discrete clock onto the unit circle to derive the imaginary unit. Quantum theorists and discrete-time modelers cite it when grounding complex phases in the Recognition Science octave. The module supplies explicit phase assignments for each tick and verifies algebraic closure properties such as rotation by 90 degrees at tick 2.

claimThe 8-tick phases are the points $e^{i k heta}$ on the unit circle for $ heta = au_0 rac{ au}{8}$ with $k = 0, o 7$, giving the cycle $1$, $(1+i)/\sqrt{2}$, $i$, $(-1+i)/\sqrt{2}$, $-1$, $(-1-i)/\sqrt{2}$, $-i$, $(1-i)/\sqrt{2}$ returning to 1 at tick 8.

background

Constants fixes the RS time quantum $ au_0 = 1$ tick. EightTick defines the fundamental discrete clock whose phases sit at multiples of $ au_0 rac{ au}{8}$ (i.e., $0$, $ au/8$, $ au/4$, $3 au/8$, $ au/2$, $5 au/8$, $3 au/4$, $7 au/8$). The present module places these phases on the complex unit circle, identifying the generator of 90-degree rotations.

proof idea

This is a definition module, no proofs. It introduces the phase map and a collection of named lemmas that record the explicit complex values and their multiplication table under the 8-tick cycle.

why it matters in Recognition Science

The module realizes the eight-tick octave (T7) as unitary rotations, supplying the complex structure required by downstream siblings such as euler_from_8tick, schrodinger_i_from_8tick and i_power_is_rotation. It therefore bridges the discrete clock to the algebraic origin of $i$ used in the Recognition Science treatment of the Schrödinger equation.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (15)