Gravity Analysis Bloch Cell Sum Exp Sum Eq Zero

The vanishing sum

The declaration expSum_eq_zero is a theorem about a sum of complex numbers that all lie on the unit circle in the complex plane. The complex plane is the two-dimensional number system where numbers have a real part and an imaginary part, and the unit circle is the set of numbers at distance exactly 1 from the origin. The theorem says: take a positive whole number N, and an integer frequency a. Consider the N numbers you get by taking the complex exponential of 2π i a j / N as j runs from 0 to N-1. These are N points evenly spaced around the unit circle. If N does not divide a, their sum is exactly 0. The companion theorem expSum_eq_card covers the other case: if N does divide a, every term equals 1, so the sum is exactly N.

This is a standard result in discrete Fourier analysis, the mathematics of breaking a periodic signal into its component frequencies. It is the discrete analogue of the fact that the integral of a sine wave over a whole number of periods is zero. The proof in the library is direct: each summand is a power of a fixed ratio, the ratio is an N-th root of unity, and a geometric series with ratio not equal to 1 sums to zero. The theorem is pure mathematics; it makes no statement about physics, gravity, or any physical system.

In Recognition Science, this theorem is a building block for a larger program that studies a lattice of cells on a three-dimensional torus, a shape like the surface of a doughnut but in three dimensions. The program needs to collapse sums of products of cosine functions over all cells into a single constant term. The vanishing sum is the mechanism that makes the unwanted terms disappear. The headline result, cellSum_cos_mul_cos, states that under a condition called non-aliasing, the sum over all cells of the product of two phase-shifted cosines equals N cubed times the cosine of the phase difference, divided by 2. The vanishing sum kills the oscillating part; only the constant part survives.

The theorem does not claim anything about the value of a physical constant, nor does it derive a force law or a particle mass. It does not touch the continuum target of the larger program, which remains an open problem. It is a lemma, not a law of nature. Its role is to provide a clean, machine-checked foundation for a later calculation that has not yet been completed.

/-- GEOMETRIC EXPONENTIAL SUM, non-aliased case: if `N` does not divide the
integer frequency `a`, the sum of `exp (2 π I a j / N)` over one period
vanishes.  Geometric series with ratio `≠ 1` whose `N`-th power is `1`. -/
theorem expSum_eq_zero (N : ℕ) [NeZero N] (a : ℤ) (ha : ¬ (N : ℤ) ∣ a) :
    ∑ j : Fin N,
        Complex.exp (2 * (Real.pi : ℂ) * Complex.I * (a : ℂ) * ((j : ℕ) : ℂ) / (N : ℂ))
      = 0 := by
  have hr_ne : Complex.exp (2 * (Real.pi : ℂ) * Complex.I * (a : ℂ) / (N : ℂ)) ≠ 1 :=
    fun h => ha ((exp_ratio_eq_one_iff N a).mp h)
  calc ∑ j : Fin N,
          Complex.exp (2 * (Real.pi : ℂ) * Complex.I * (a : ℂ) * ((j : ℕ) : ℂ) / (N : ℂ))
      = ∑ j : Fin N,
          Complex.exp (2 * (Real.pi : ℂ) * Complex.I * (a : ℂ) / (N : ℂ)) ^ (j : ℕ) :=
        Finset.sum_congr rfl fun j _ => exp_term_eq_pow N a j
    _ = ∑ j ∈ Finset.range N,
          Complex.exp (2 * (Real.pi : ℂ) * Complex.I * (a : ℂ) / (N : ℂ)) ^ j :=
        Fin.sum_univ_eq_sum_range
          (fun k => Complex.exp (2 * (Real.pi : ℂ) * Complex.I * (a : ℂ) / (N : ℂ)) ^ k) N
    _ = (Complex.exp (2 * (Real.pi : ℂ) * Complex.I * (a : ℂ) / (N : ℂ)) ^ N - 1)
          / (Complex.exp (2 * (Real.pi : ℂ) * Complex.I * (a : ℂ) / (N : ℂ)) - 1) :=
        geom_sum_eq hr_ne N
    _ = 0 := by rw [exp_ratio_pow_card N a, sub_self, zero_div]

/-- GEOMETRIC EXPONENTIAL SUM, aliased case: if `N` divides the integer
frequency `a`, every summand is `1` and the sum equals `N`. -/
theorem expSum_eq_card (N : ℕ) [NeZero N] (a : ℤ) (ha : (N : ℤ) ∣ a) :
    ∑ j : Fin N,
        Complex.exp (2 * (Real.pi : ℂ) * Complex.I * (a : ℂ) * ((j : ℕ) : ℂ) / (N : ℂ))
      = (N : ℂ) := by
  obtain ⟨c, rfl⟩ := ha
  have hN : (N : ℂ) ≠ 0 := Nat.cast_ne_zero.mpr (NeZero.ne N)
  have hterm : ∀ j : Fin N,
      Complex.exp
          (2 * (Real.pi : ℂ) * Complex.I * (((N : ℤ) * c : ℤ) : ℂ) * ((j : ℕ) : ℂ) / (N : ℂ))
        = 1 := by
    intro j
    have harg :
        2 * (Real.pi : ℂ) * Complex.I * (((N : ℤ) * c : ℤ) : ℂ) * ((j : ℕ) : ℂ) / (N : ℂ)
          = ((c * (j : ℕ) : ℤ) : ℂ) * (2 * (Real.pi : ℂ) * Complex.I) := by
      rw [div_eq_iff hN]
      push_cast
      ring
    rw [harg]
    exact Complex.exp_int_mul_two_pi_mul_I _
  calc ∑ j : Fin N,
          Complex.exp
            (2 * (Real.pi : ℂ) * Complex.I * (((N : ℤ) * c : ℤ) : ℂ) * ((j : ℕ) : ℂ) / (N : ℂ))
      = ∑ _j : Fin N, (1 : ℂ) := Finset.sum_congr rfl fun j _ => hterm j
    _ = (N : ℂ) := by
        simp only [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul, mul_one]

What this page does not claim

This theorem makes no statement about gravity, forces, or any physical system. The theorem does not derive any physical constant or particle mass. The continuum target of the larger program remains open and is not established by this lemma.

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/Gravity/Analysis/BlochCellSum.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: