Mathematics Complex Numbers Tick Phases Equally Spaced

The equally spaced phases

Complex numbers are the number system built from a real part and an imaginary part, where the imaginary unit i squares to -1. They first became indispensable in the 16th century for solving cubic equations, and later became the natural language for anything that oscillates or rotates. A point moving in a circle can be described by a complex number of the form e^(iθ), which traces the unit circle as the angle θ grows; multiplying two such numbers adds their angles, so complex multiplication is rotation in the plane.

The framework's declaration tick_phases_equally_spaced concerns eight specific points on that circle. In Recognition Science, a ledger, a discrete record of events, runs through an eight-tick cycle, and each tick is assigned a phase angle. The theorem states that the ratio of any two of these eight phase points is again a complex exponential whose angle is an integer multiple of π/4, which is 45 degrees. In plainer terms: the eight phases are exactly the eighth roots of unity, spaced evenly around the circle like the hours on a clock face, and the gap between any two of them is a whole number of 45-degree steps.

This even spacing is what makes the set a cyclic group under multiplication. Because the phases close under multiplication and division, they describe rotations that can be composed and inverted, which is precisely what a phase structure needs to do. The theorem is proved in the machine-checked library of formal theorems, and its proof is a direct calculation: it expands each phase as e^(iπk/4), uses the fact that division of exponentials subtracts their exponents, and simplifies the algebra to the claimed angle.

What the theorem does not claim is larger. It does not claim that physics must use complex numbers, nor that the eight-tick cycle itself is forced, nor that the phases correspond to any particular physical quantity. Those are separate statements in the framework, some proved and some not. The equally-spaced theorem only pins down the geometry of the eight phase points once they are defined as they are. It is a precise structural fact about a chosen set of points, not an argument that the universe runs on that set.

/-- The phases are equally spaced around the unit circle.
    Consecutive phases differ by π/4 (45°). -/
theorem tick_phases_equally_spaced (j k : Fin 8) (hjk : j < k) :
    -- The quotient tickPhase k / tickPhase j has argument (k - j) * π/4 modulo 2π
    tickPhase k / tickPhase j = Complex.exp ((k.val - j.val : ℝ) * π / 4 * I) := by
  unfold tickPhase
  -- Use exp_sub: exp(a) / exp(b) = exp(a - b)
  rw [← Complex.exp_sub]
  congr 1
  -- Show: I * π * k / 4 - I * π * j / 4 = (k - j) * π / 4 * I
  push_cast
  ring

/-- **THEOREM**: The 8 tick phases are 8th roots of unity. -/
theorem tick_phases_roots_of_unity (k : Fin 8) :
    (tickPhase k)^8 = 1 := by
  unfold tickPhase
  -- exp(I × π × k / 4)^8 = exp(8 × I × π × k / 4) = exp(2πIk) = 1
  rw [← Complex.exp_nat_mul]
  have h : (8 : ℕ) * (I * ↑π * ↑(k : ℕ) / 4) = ↑(k : ℕ) * (2 * ↑π * I) := by
    push_cast
    ring
  rw [h]
  exact Complex.exp_nat_mul_two_pi_mul_I k

What this page does not claim

The theorem does not prove that physics requires complex numbers. The theorem does not establish that the eight-tick cycle is necessary. The theorem does not identify the phases with any specific physical observable.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Mathematics/ComplexNumbers.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: