Encyclopedia Foundation Foundation Eight Tick Sum 8 Phases Eq Zero
ARTICLE 4 claims 3 theorems 1 model
Foundation Eight Tick Sum 8 Phases Eq Zero
Eight equally spaced points on a circle always balance to zero, a fact that Recognition Science uses as the foundation for its account of vacuum fluctuations.
The vanishing sum
The sum of the eight eighth roots of unity is zero. Written out, this is 1 + ζ + ζ² + ... + ζ⁷ = 0, where ζ = exp(iπ/4) is the complex number at 45 degrees on the unit circle. This is a classical result: the eight roots of unity are the vertices of a regular octagon centered at the origin, and their average position is the center itself. The theorem sum_8_phases_eq_zero in the framework's machine-checked library of formal theorems establishes exactly this identity for the eight phases kπ/4 for k = 0, 1, ..., 7, using the complex exponential exp(i × k × π/4).
The identity is a statement about complex numbers, not about physics. It says that if you take the eight complex numbers obtained by rotating the point 1 by multiples of 45 degrees and add them, you get 0. The proof is a direct computation: each phase is a root of unity, and the sum of all n-th roots of unity is 0 for any n greater than 1. The framework's declaration packages this classical fact under its discrete 8-tick structure, where the phases are indexed by k = 0, 1, ..., 7 and the sum is taken over all eight indices.
In Recognition Science, this vanishing sum is called the foundation of vacuum fluctuation cancellation. The idea is that the eight phases represent a complete cycle, and their balanced sum corresponds to a net zero contribution. The framework models this as the starting point for deriving properties like spin-statistics, where the phase at k=4 gives -1 (the fermion antisymmetry sign) and the phase at k=0 gives 1 (the boson symmetry sign). The sum being zero is the discrete analogue of a full cycle averaging out.
What the declaration does not claim is equally important. It does not prove that vacuum fluctuations actually cancel in physical reality; it only establishes the mathematical identity that the framework uses as a premise. The step from the algebraic fact (the sum is zero) to a physical statement about the vacuum is a modeling choice, not a theorem. The declaration also does not claim that the eight phases are the only possible discrete clock, nor does it derive the number 8 from more basic principles; the 8-tick structure is taken as a definitional starting point within the framework.
The practical consequence is that the framework has a rigorously established algebraic foundation for its discrete cycle. The sum being zero is a necessary condition for any theory that wants to treat the eight phases as a balanced whole, and the machine-checked proof guarantees that this condition holds without hidden assumptions. A reader can now see that the framework's discrete clock is internally consistent at the level of complex arithmetic, even before any physical interpretation is attached.
THEOREM sum_8_phases_eq_zero · IndisputableMonolith/Foundation/EightTick.lean
/-- 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)
THEOREM sum_8_phases_eq_zero · IndisputableMonolith/Foundation/EightTick.lean
/-- 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)
MODEL sum_8_phases_eq_zero · IndisputableMonolith/Foundation/EightTick.lean
/-- 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)
THEOREM spin_statistics_key · IndisputableMonolith/Foundation/EightTick.lean
/-- **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⟩
What this page does not claim
The declaration does not prove that vacuum fluctuations physically cancel. The declaration does not derive the 8-tick structure from more basic principles. The declaration does not establish that the eight phases are 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:
- How does the framework derive the number 8 from more basic principles, if at all?
- What physical mechanism connects the algebraic vanishing sum to actual vacuum fluctuation cancellation?
- Does the framework's 8-tick structure uniquely determine the spin-statistics connection, or are other discrete clocks possible?
- What is the precise definition of tau0 that appears in the fundamental frequency?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM sum_8_phases_eq_zero · IndisputableMonolith/Foundation/EightTick.lean
/-- 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)The sum of the eight eighth roots of unity is zero. sum_8_phases_eq_zero · IndisputableMonolith/Foundation/EightTick.leanTHEOREM sum_8_phases_eq_zero · IndisputableMonolith/Foundation/EightTick.lean
/-- 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)The theorem sum_8_phases_eq_zero in the framework's machine-checked library of formal theorems establishes exactly this identity for the eight phases kπ/4 for k = 0, 1, ..., 7. sum_8_phases_eq_zero · IndisputableMonolith/Foundation/EightTick.leanMODEL sum_8_phases_eq_zero · IndisputableMonolith/Foundation/EightTick.lean
/-- 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)In Recognition Science, this vanishing sum is called the foundation of vacuum fluctuation cancellation. sum_8_phases_eq_zero · IndisputableMonolith/Foundation/EightTick.leanTHEOREM spin_statistics_key · IndisputableMonolith/Foundation/EightTick.lean
/-- **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 phase at k=4 gives -1 (the fermion antisymmetry sign) and the phase at k=0 gives 1 (the boson symmetry sign). spin_statistics_key · IndisputableMonolith/Foundation/EightTick.lean