Foundation Eight Tick Eight Tick Generates Z8

The eight-tick clock

The declaration eight_tick_generates_Z8 establishes a precise algebraic fact about a discrete clock. The clock has eight ticks, or phases, spaced by quarter turns: 0, π/4, π/2, 3π/4, π, 5π/4, 3π/2, and 7π/4. The theorem proves that every one of these eight phases can be written as a power of the first tick, the phase at π/4. In the language of group theory, this means the eight phases form a cyclic group of order eight, written Z/8Z. The proof is machine-checked, meaning a computer program verified each step of the argument.

The result is a structural statement about the clock itself, not a claim about any physical system. It says that the eight phases are generated by repeated application of a single step, the step from one tick to the next. This is what makes the structure a cycle: starting at phase zero and advancing by one tick eight times returns to the start. The theorem also shows that the eighth power of each phase equals one, a property of the eighth roots of unity. These roots are the complex numbers that, when raised to the eighth power, give 1.

In Recognition Science, this cycle is not an isolated piece of mathematics. The framework models reality as a discrete record of events, and the eight-tick cycle is the fundamental clock of that record. The phases are used to represent symmetry operations, with even ticks assigned to bosons and odd ticks to fermions. The theorem that the phases generate Z/8Z is the algebraic backbone of these assignments, showing that the symmetry group is cyclic and generated by a single tick.

The declaration does not claim that the eight-tick cycle is the only possible clock, nor does it prove that any physical particle must follow this cycle. It establishes a property of a defined mathematical object, the phase function on eight points. The connection to spin and statistics is a modeling choice within the framework, not a consequence of this theorem alone. The theorem is a piece of pure algebra about a specific set of complex numbers.

/-- The 8-tick structure generates the group ℤ/8ℤ.
    This is isomorphic to the discrete symmetry group of RS. -/
theorem eight_tick_generates_Z8 :
    ∀ k : Fin 8, ∃ n : ℕ, phaseExp k = (phaseExp ⟨1, by norm_num⟩)^n := by
  intro k
  use k.val
  unfold phaseExp phase
  rw [← Complex.exp_nat_mul]
  congr 1
  push_cast
  ring

/-- **THEOREM**: The 8th power of each phase gives 1.
    exp(i × k × π/4)^8 = exp(2πik) = 1.
    Uses periodicity: exp(2πin) = 1 for n ∈ ℤ. -/
theorem phase_eighth_power_is_one (k : Fin 8) :
    (phaseExp k)^8 = 1 := by
  unfold phaseExp phase
  rw [← Complex.exp_nat_mul]
  -- 8 * (I * (k * π / 4)) = 2kπI, and exp(2kπI) = 1
  have h : (8 : ℕ) * (Complex.I * ((k.val : ℕ) * Real.pi / 4 : ℝ)) = 2 * Real.pi * Complex.I * k.val := by
    push_cast
    ring
  simp only [] at h
  rw [show (k : ℕ) = k.val from rfl] at h ⊢
  convert Complex.exp_int_mul_two_pi_mul_I k.val using 2
  push_cast
  ring

What this page does not claim

This theorem does not prove that any physical system must follow an eight-tick cycle. This theorem does not establish the spin-statistics connection; that is a modeling choice in the framework. This theorem does not claim that the eight-tick cycle is the only possible discrete clock.

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/Foundation/EightTick.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: