tickPhase
The tickPhase definition assigns to each k in Fin 8 the complex value exp(i π k /4), encoding the phase of the k-th tick in the recognition cycle. Researchers deriving the necessity of complex numbers from the eight-tick ledger would cite this construction. It is realized as a direct one-line definition via the complex exponential.
claimFor each integer $k$ with $0 ≤ k ≤ 7$, the phase of the $k$-th recognition tick is defined by $e^{i π k / 4}$.
background
In Recognition Science the fundamental time unit is the tick, denoted τ₀ and set to 1 in native units. The eight-tick octave is the self-similar period forced by the phi-ladder and J-uniqueness. Module MATH-004 derives that these phases must be realized as rotations in the plane, which requires the complex numbers ℂ.
proof idea
The definition is a direct one-line assignment that applies Complex.exp to the scaled imaginary unit I * π * k / 4. No lemmas are invoked beyond the built-in definition of the complex exponential.
why it matters in Recognition Science
This supplies the concrete phase map used by downstream results such as tick_phases_roots_of_unity and phases_require_complex to show the phases are eighth roots of unity and that non-real components exist. It implements the T7 eight-tick octave step and supports the claim that complex numbers are forced by the ledger cycle, as stated in the module documentation.
scope and limits
- Does not prove that the phases must be realized in ℂ rather than another 2D algebra.
- Does not derive the eight-tick period from more primitive axioms.
- Does not compute physical observables or coupling constants from the phases.
- Does not address experimental measurability of the phases.
Lean usage
unfold tickPhaseformal statement (Lean)
50noncomputable def tickPhase (k : Fin 8) : ℂ :=
proof body
Definition body.
51 Complex.exp (I * π * k / 4)
52
53/-- **THEOREM**: The 8 tick phases are 8th roots of unity. -/