Foundation Eight Tick Phase 4 Is Minus One

The half-cycle sign

The eighth roots of unity are the eight complex numbers whose eighth power is 1. They sit evenly spaced around the unit circle in the complex plane, at angles 0, π/4, π/2, 3π/4, π, 5π/4, 3π/2, and 7π/4. The fourth of these, at angle π, is the number -1. This is elementary: multiplying -1 by itself eight times gives 1, and no smaller positive power does.

Recognition Science (RS) builds a discrete clock from these eight positions, calling each position a tick, a single step in a repeating cycle of eight. The framework's machine-checked library of formal theorems establishes that the complex exponential of the fourth tick equals -1. The declaration phase_4_is_minus_one states this result: exp(i × 4 × π/4) = exp(iπ) = -1. The same library establishes that the zeroth tick gives 1, and the two together form the spin-statistics key theorem.

The sign matters because it is the mathematical fingerprint of exchange. In quantum mechanics, swapping two identical particles multiplies their joint wavefunction by a phase. If the phase is +1, the particles are bosons, which can pile into the same quantum state. If the phase is -1, the particles are fermions, which must avoid one another. The framework identifies the +1 with the zeroth tick and the -1 with the fourth tick, a half-cycle of its fundamental clock. The theorem itself is a fact about complex numbers; the identification with particle behavior is the framework's modeling choice.

What the theorem does not do is establish the spin-statistics connection from scratch. It establishes the algebraic identity that the fourth tick is -1. The bridge from that identity to the exclusion principle, and to the framework's broader claims about CPT symmetry and gauge groups, is a program of interpretation, not a single established step. The library also shows the eight ticks generate the cyclic group ℤ/8ℤ and that all eight phases sum to zero, facts the framework uses as scaffolding for later derivations.

/-- Phase at k=4 gives -1 (fermion phase).
    This is the key to antisymmetry under particle exchange. -/
theorem phase_4_is_minus_one : phaseExp ⟨4, by norm_num⟩ = -1 := by
  unfold phaseExp phase
  have h : Complex.I * ((4 : ℕ) * Real.pi / 4 : ℝ) = Real.pi * Complex.I := by
    push_cast
    ring
  rw [h, Complex.exp_pi_mul_I]

/-- Phase at k=0 gives 1 (boson phase).
    This is the identity phase - no change under exchange. -/
theorem phase_0_is_one : phaseExp ⟨0, by norm_num⟩ = 1 := by
  unfold phaseExp phase
  simp only [Nat.cast_zero, zero_mul, zero_div, mul_zero, Complex.ofReal_zero,
             Complex.exp_zero]

/-- **SPIN-STATISTICS KEY THEOREM**:
    Phase k=4 (half-cycle) gives -1, which is the fermion antisymmetry sign.
    Phase k=0 (identity) gives 1, which is the boson symmetry sign.
    This connects 8-tick structure to spin-statistics. -/
theorem spin_statistics_key :
    phaseExp ⟨4, by norm_num⟩ = -1 ∧ phaseExp ⟨0, by norm_num⟩ = 1 :=
  ⟨phase_4_is_minus_one, phase_0_is_one⟩

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

/-- Sum of all 8 phases equals zero (roots of unity).
    This is the foundation of vacuum fluctuation cancellation.
    The 8th roots of unity sum to 0: 1 + ζ + ζ² + ... + ζ⁷ = 0 where ζ = exp(iπ/4). -/
theorem sum_8_phases_eq_zero :
    ∑ k : Fin 8, phaseExp k = 0 := by
  -- The sum of n-th roots of unity is 0 for n > 1
  -- Let ζ = exp(2πi/8) = exp(iπ/4), a primitive 8th root of unity
  let ζ : ℂ := Complex.exp (2 * Real.pi * Complex.I / 8)
  -- ζ is a primitive 8th root of unity
  have hζ_prim : IsPrimitiveRoot ζ 8 := by
    have h8pos : (8 : ℕ) ≠ 0 := by norm_num
    exact Complex.isPrimitiveRoot_exp 8 h8pos
  -- Show that phaseExp k = ζ^k
  have h_phase_as_power : ∀ k : Fin 8, phaseExp k = ζ ^ (k : ℕ) := by
    intro k
    unfold phaseExp phase ζ
    rw [← Complex.exp_nat_mul]
    congr 1
    push_cast
    ring
  -- Rewrite the sum using powers of ζ
  have h_sum_eq : ∑ k : Fin 8, phaseExp k = ∑ k : Fin 8, ζ ^ (k : ℕ) := by
    congr 1
    ext k
    exact h_phase_as_power k
  rw [h_sum_eq]
  -- Transform to the range form
  have h_geom : ∑ k : Fin 8, ζ ^ (k : ℕ) = ∑ k ∈ Finset.range 8, ζ ^ k := by
    rw [Fin.sum_univ_eq_sum_range]
  rw [h_geom]
  -- Apply the primitive root theorem: sum of primitive roots = 0
  exact hζ_prim.geom_sum_eq_zero (by norm_num : 1 < 8)

What this page does not claim

The theorem does not establish the spin-statistics connection from physical principles; it establishes an algebraic identity about complex numbers. The theorem does not establish that physical particles are governed by the framework's eight-tick clock; that identification is a modeling choice. The theorem does not derive the framework's broader claims about CPT symmetry or gauge group structure.

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: