eightTickPhase
plain-language theorem explainer
eightTickPhase assigns to each n in the eight-element set of discrete ticks the complex phase exp(i n π /4) on the unit circle. Researchers deriving the imaginary unit from discrete time structures cite it to ground phase rotations in an eight-tick clock. The definition is realized by a single closed-form expression using the complex exponential.
Claim. For each integer $n$ with $0 ≤ n ≤ 7$, the phase of tick $n$ is $e^{i n π / 4}$.
background
Recognition Science treats time as discrete ledger ticks rather than a continuous manifold. The upstream Tick structure is defined by a natural-number index with the eight-tick variant restricting indices to Fin 8 so that the cycle closes after eight steps. Module MATH-001 sets the local goal of obtaining i² = -1 from this phase structure, where a two-tick rotation generates multiplication by i.
proof idea
The definition is a direct one-line expression that maps n to the complex exponential of I times (n cast to real) times π divided by 4. No lemmas or tactics are applied; the body is the primitive assignment of phases to the eight ticks.
why it matters
This definition supplies the phase map used by downstream theorems tick2_is_i and tick4_is_neg1 to identify specific ticks with i and -1. It feeds the parent result schrodinger_i_from_8tick that places the imaginary unit in the Schrödinger equation as the eight-tick generator. The construction realizes the eight-tick octave landmark and accounts for the appearance of complex numbers in quantum mechanics within the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.