Encyclopedia Gravity Gravity Analysis Bloch Cell Sum Cos Sum Eq Zero

ARTICLE 3 claims 3 theorems

Gravity Analysis Bloch Cell Sum Cos Sum Eq Zero

A simple trigonometric identity, proved in the framework's machine-checked library, shows when a sum of cosine waves cancels to zero.

Verify this page

A sum that vanishes

The declaration cosSum_eq_zero is a theorem about a sum of cosine values. It states that if you take a cosine whose angle increases in equal steps, cos(2π a j / N + φ), and sum it over one full period, j = 0, 1, ..., N-1, the total is exactly zero, provided the integer a is not a multiple of N. The phase shift φ can be any constant; it does not affect the result. This is a standard fact from discrete Fourier analysis, and the framework's library proves it using only the geometric series formula.

The theorem is part of a larger toolkit for simplifying sums over a three-dimensional grid of cells. A related headline result, cellSum_cos_mul_cos, uses this one-dimensional fact to show that a sum of products of two cosines over a torus collapses to a simple constant, N³ cos(α - β) / 2, whenever the doubled frequency is non-aliased. The non-aliasing condition means that on at least one axis, 2mi is not divisible by N. This is the kind of identity that appears when analyzing waves on a lattice.

In Recognition Science, this identity is a tool for a specific program: simplifying sums that arise in a proposed model of quantum gravity. The framework's library proves it as a pure mathematical statement, with no physics assumptions. The theorem itself is about discrete sums of cosines, nothing more. It does not, by itself, say anything about gravity, space, or any physical quantity. The downstream use of this identity in a physics calculation is a separate step, and that step is not part of this theorem.

The proof is fully checked by a machine, with no gaps or unproven assumptions. The library's audit shows it relies only on the standard axioms of the underlying logic, not on any framework-specific postulates. This makes the theorem a solid foundation for the larger program, even though that program's physical conclusions remain open targets.

THEOREM cosSum_eq_zero · IndisputableMonolith/Gravity/Analysis/BlochCellSum.lean
cosSum_eq_zero · IndisputableMonolith/Gravity/Analysis/BlochCellSum.lean:191 
/-- COSINE PHASE SUM (1D): if `N` does not divide the integer frequency `a`,
the cosine sum over one period vanishes for every constant phase `φ`. -/
theorem cosSum_eq_zero (N : ℕ) [NeZero N] (a : ℤ) (ha : ¬ (N : ℤ) ∣ a) (φ : ℝ) :
    ∑ j : Fin N,
        Real.cos (2 * Real.pi * (a : ℝ) * ((j : ℕ) : ℝ) / (N : ℝ) + φ) = 0 := by
  refine sum_cos_of_sum_exp_eq_zero
    (fun j : Fin N => 2 * Real.pi * (a : ℝ) * ((j : ℕ) : ℝ) / (N : ℝ)) φ ?_
  have hbridge : ∀ j : Fin N,
      Complex.exp (((2 * Real.pi * (a : ℝ) * ((j : ℕ) : ℝ) / (N : ℝ) : ℝ)) * Complex.I : ℂ)
        = Complex.exp
            (2 * (Real.pi : ℂ) * Complex.I * (a : ℂ) * ((j : ℕ) : ℂ) / (N : ℂ)) := by
    intro j
    congr 1
    push_cast
    ring
  exact (Finset.sum_congr rfl fun j _ => hbridge j).trans (expSum_eq_zero N a ha)
THEOREM expSum_eq_zero · IndisputableMonolith/Gravity/Analysis/BlochCellSum.lean
expSum_eq_zero · IndisputableMonolith/Gravity/Analysis/BlochCellSum.lean:112 
/-- 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]
THEOREM cellSum_cos_mul_cos · IndisputableMonolith/Gravity/Analysis/BlochCellSum.lean
cellSum_cos_mul_cos · IndisputableMonolith/Gravity/Analysis/BlochCellSum.lean:326 
/-- HEADLINE (PRODUCT-TO-SUM BLOCH CELL SUM): for a commensurate wave vector
`k = 2 π m / N` whose doubled frequency `2 m` is non-aliased on some axis
(`∃ i, ¬ (N : ℤ) ∣ 2 * m i`), the torus cell-sum of the product of two
phase-shifted cosines collapses to the constant term:
`∑ x, cos (theta N m x + α) * cos (theta N m x + β) = N ^ 3 * cos (α - β) / 2`.
The `(A - B)` half of the product-to-sum identity is constant and
contributes `N ^ 3 * cos (α - β) / 2`; the `(A + B)` half is a cell-sum at
doubled frequency and vanishes by `cellSum_cos_eq_zero`. -/
theorem cellSum_cos_mul_cos (N : ℕ) [NeZero N] (m : Fin 3 → ℤ) (α β : ℝ)
    (halias : ∃ i : Fin 3, ¬ (N : ℤ) ∣ 2 * m i) :
    ∑ x : Fin N × Fin N × Fin N,
        Real.cos (theta N m x + α) * Real.cos (theta N m x + β)
      = (N : ℝ) ^ 3 * Real.cos (α - β) / 2 := by
  have hzero :
      ∑ x : Fin N × Fin N × Fin N,
          Real.cos (theta N (fun i => 2 * m i) x + (α + β)) = 0 :=
    cellSum_cos_eq_zero N (fun i => 2 * m i) halias (α + β)
  have hpt : ∀ x : Fin N × Fin N × Fin N,
      Real.cos (theta N m x + α) * Real.cos (theta N m x + β)
        = Real.cos (α - β) / 2
          + Real.cos (theta N (fun i => 2 * m i) x + (α + β)) / 2 := by
    intro x
    rw [cos_mul_cos]
    rw [show theta N m x + α - (theta N m x + β) = α - β from by ring]
    rw [show theta N m x + α + (theta N m x + β) = 2 * theta N m x + (α + β) from by ring]
    rw [← theta_two_mul N m x]
    ring
  calc ∑ x : Fin N × Fin N × Fin N,
          Real.cos (theta N m x + α) * Real.cos (theta N m x + β)
      = ∑ x : Fin N × Fin N × Fin N,
          (Real.cos (α - β) / 2
            + Real.cos (theta N (fun i => 2 * m i) x + (α + β)) / 2) :=
        Finset.sum_congr rfl fun x _ => hpt x
    _ = (∑ _x : Fin N × Fin N × Fin N, Real.cos (α - β) / 2)
          + ∑ x : Fin N × Fin N × Fin N,
              Real.cos (theta N (fun i => 2 * m i) x + (α + β)) / 2 :=
        Finset.sum_add_distrib
    _ = (N : ℝ) ^ 3 * Real.cos (α - β) / 2 := by
        have hconst : (∑ _x : Fin N × Fin N × Fin N, Real.cos (α - β) / 2)
            = (N : ℝ) ^ 3 * Real.cos (α - β) / 2 := by
          simp only [Finset.sum_const, Finset.card_univ, Fintype.card_prod,
            Fintype.card_fin, nsmul_eq_mul]
          push_cast
          ring
        have hosc : (∑ x : Fin N × Fin N × Fin N,
              Real.cos (theta N (fun i => 2 * m i) x + (α + β)) / 2) = 0 := by
          simp only [div_eq_mul_inv, ← Finset.sum_mul]
          rw [hzero, zero_mul]
        rw [hconst, hosc, add_zero]

What this page does not claim

This theorem makes no statement about gravity or any physical system. The proof does not introduce any new axioms beyond the standard logical ones. The identity does not prove the continuum target it is intended to support.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND