Mathematics Complex Numbers Tick Phases Roots Of Unity

The eighth roots of unity

The eighth roots of unity are the eight complex numbers that solve z^8 = 1. They sit evenly spaced on the unit circle in the complex plane, at angles that are multiples of 45 degrees: 0, 45, 90, 135, 180, 225, 270, and 315 degrees. Multiplying by one of them rotates a point on the circle by that angle, and multiplying by the same root eight times brings any point back to where it started. These numbers are the standard mathematical description of an eight-step cycle of rotation.

This classical object appears in the framework's account of its fundamental recognition cycle, a discrete record of events the framework uses as its basic unit of process. The framework's library, a machine-checked collection of formal theorems, defines a tick phase as the complex number e^(iπk/4) for k = 0 through 7. The theorem tick_phases_roots_of_unity proves that raising any of these eight phases to the eighth power gives exactly 1, which is the defining property of an eighth root of unity. A second theorem proves the phases are equally spaced, so the eight points form a regular octagon on the circle.

In Recognition Science, these phases are the framework's model for why physics needs complex numbers. The framework's account observes that rotations in a plane require two dimensions, and that complex multiplication naturally performs such rotations. Its library proves that the phases at 45 and 90 degrees have nonzero imaginary parts, meaning they cannot be represented by real numbers alone. The framework presents this as the reason quantum mechanics, electromagnetism, and signal processing all use complex numbers: their shared cyclic structure is, in this account, the same eight-tick cycle.

What the declaration does not claim is broader than what it proves. The theorem establishes a property of a definition, not the necessity of that definition. The framework's library also contains statements, tagged as theorems, that the eight-tick structure leads to complex numbers and that complex numbers are inevitable, but these are given as trivial True statements in the code, not as substantive proofs. The claim that experiments rule out real-number quantum mechanics is listed as a prediction with a named falsifier, not as a proved result. The theorem itself, tick_phases_roots_of_unity, only says that the defined phases satisfy z^8 = 1; the interpretive leap from that algebraic fact to the structure of physics is a separate, less formal claim.

/-- **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

/-- 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**: 8-tick phases require rotation, which requires ℂ.
    The first non-trivial phase (k=1) has nonzero imaginary part. -/
theorem phases_require_complex_k1 : (tickPhase ⟨1, by omega⟩).im ≠ 0 := by
  unfold tickPhase
  -- exp(I * π / 4) = cos(π/4) + I * sin(π/4)
  have h : I * ↑π * ↑(1 : ℕ) / 4 = ↑(π / 4 : ℝ) * I := by push_cast; ring
  simp only [show (⟨1, by omega⟩ : Fin 8).val = 1 from rfl] at *
  rw [h, Complex.exp_mul_I]
  rw [← Complex.ofReal_cos, ← Complex.ofReal_sin]
  simp only [Complex.add_im, Complex.mul_I_im, Complex.ofReal_im, Complex.ofReal_re, zero_add]
  -- sin(π/4) = √2/2 ≠ 0
  rw [Real.sin_pi_div_four]
  exact ne_of_gt (by positivity)

/-- The phase at k=2 (which is π/2) also has nonzero imaginary part. -/
theorem phases_require_complex_k2 : (tickPhase ⟨2, by omega⟩).im ≠ 0 := by
  unfold tickPhase
  have h : I * ↑π * ↑(2 : ℕ) / 4 = ↑(π / 2 : ℝ) * I := by push_cast; ring
  simp only [show (⟨2, by omega⟩ : Fin 8).val = 2 from rfl] at *
  rw [h, Complex.exp_mul_I]
  rw [← Complex.ofReal_cos, ← Complex.ofReal_sin]
  simp only [Complex.add_im, Complex.mul_I_im, Complex.ofReal_im, Complex.ofReal_re, zero_add]
  rw [Real.sin_pi_div_two]
  norm_num

What this page does not claim

The theorem does not prove that complex numbers are necessary for physics; it only proves a property of a definition. The framework's statements that complex numbers are inevitable are trivial True declarations, not substantive proofs. The claim that experiments rule out real quantum mechanics is a prediction with a falsifier, not a proved theorem.

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: