Encyclopedia Gravity Gravity Analysis Bloch Cell Sum Cell Sum Cos Eq Zero

ARTICLE 4 claims 3 theorems 1 model

Gravity Analysis Bloch Cell Sum Cell Sum Cos Eq Zero

A machine-checked theorem shows that certain sums of cosine waves over a three-dimensional grid always cancel to zero, a fact the framework's gravity program relies on.

Verify this page

The vanishing cell sum

The declaration cellSum_cos_eq_zero is a theorem about a specific kind of sum. A three-dimensional grid of points, with N points along each edge. At every point, place a cosine wave whose phase is a linear combination of the point's coordinates, plus some fixed offset. The theorem says: if the wave's frequency vector has at least one component that is not an integer multiple of N, then the sum of the cosine values over all N³ grid points is exactly zero. This holds for any constant phase offset. It is a pure statement about discrete Fourier orthogonality, a classical tool in digital signal processing and solid-state physics.

The proof is a chain of elementary steps. A one-dimensional geometric sum of complex exponentials vanishes when its frequency is not a multiple of N. Taking the real part of that sum gives the same result for cosines. The three-dimensional sum factorizes into a product of three one-dimensional sums, so if any one of them vanishes, the whole product does. The theorem is verified in the framework's machine-checked library of formal theorems, with no unproved assumptions beyond the standard axioms of the underlying logic.

In Recognition Science, this identity is not an isolated curiosity. The framework's gravity program uses it to simplify sums that appear when analyzing a continuum limit. The consumer program needs to collapse sums of products of two cosines into a single cosine of a phase difference. The vanishing of the sum of a single cosine is the step that makes that collapse possible. The framework models this as a necessary piece of the machinery, not as a physical claim about gravity itself.

The theorem does not claim anything about the physical world. It says nothing about the value of the continuum target, which the library keeps as an open problem. It does not assert that any particular grid or wave exists in nature. It is a statement about the algebra of trigonometric sums on a finite grid, and nothing more.

THEOREM cellSum_cos_eq_zero · IndisputableMonolith/Gravity/Analysis/BlochCellSum.lean
cellSum_cos_eq_zero · IndisputableMonolith/Gravity/Analysis/BlochCellSum.lean:303 
/-- 3D COSINE CELL-SUM VANISHING: if some component frequency `m i` is not
divisible by `N`, the cosine cell-sum with any constant phase `φ` vanishes.
The 3D exponential sum factorizes and the non-aliased axis kills the
product. -/
theorem cellSum_cos_eq_zero (N : ℕ) [NeZero N] (m : Fin 3 → ℤ)
    (h : ∃ i : Fin 3, ¬ (N : ℤ) ∣ m i) (φ : ℝ) :
    ∑ x : Fin N × Fin N × Fin N, Real.cos (theta N m x + φ) = 0 := by
  refine sum_cos_of_sum_exp_eq_zero (theta N m) φ ?_
  rw [cellSum_exp_eq_prod N m]
  obtain ⟨i, hi⟩ := h
  fin_cases i
  · exact mul_eq_zero_of_left (mul_eq_zero_of_left (expSum_eq_zero N (m 0) hi) _) _
  · exact mul_eq_zero_of_left (mul_eq_zero_of_right _ (expSum_eq_zero N (m 1) hi)) _
  · exact mul_eq_zero_of_right _ (expSum_eq_zero N (m 2) hi)
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_exp_eq_prod · IndisputableMonolith/Gravity/Analysis/BlochCellSum.lean
cellSum_exp_eq_prod · IndisputableMonolith/Gravity/Analysis/BlochCellSum.lean:236 
/-- The 3D cell exponential sum factorizes into the product of the three 1D
geometric exponential sums (one per axis). -/
theorem cellSum_exp_eq_prod (N : ℕ) [NeZero N] (m : Fin 3 → ℤ) :
    ∑ x : Fin N × Fin N × Fin N, Complex.exp ((theta N m x : ℂ) * Complex.I)
      = (∑ j : Fin N,
            Complex.exp (2 * (Real.pi : ℂ) * Complex.I * (m 0 : ℂ) * ((j : ℕ) : ℂ) / (N : ℂ)))
        * (∑ j : Fin N,
            Complex.exp (2 * (Real.pi : ℂ) * Complex.I * (m 1 : ℂ) * ((j : ℕ) : ℂ) / (N : ℂ)))
        * (∑ j : Fin N,
            Complex.exp (2 * (Real.pi : ℂ) * Complex.I * (m 2 : ℂ) * ((j : ℕ) : ℂ) / (N : ℂ))) := by
  have hsplit : ∀ x : Fin N × Fin N × Fin N,
      Complex.exp ((theta N m x : ℂ) * Complex.I)
        = Complex.exp
            (2 * (Real.pi : ℂ) * Complex.I * (m 0 : ℂ) * ((x.1 : ℕ) : ℂ) / (N : ℂ))
          * (Complex.exp
              (2 * (Real.pi : ℂ) * Complex.I * (m 1 : ℂ) * ((x.2.1 : ℕ) : ℂ) / (N : ℂ))
            * Complex.exp
              (2 * (Real.pi : ℂ) * Complex.I * (m 2 : ℂ) * ((x.2.2 : ℕ) : ℂ) / (N : ℂ))) := by
    intro x
    rw [← Complex.exp_add, ← Complex.exp_add]
    congr 1
    simp only [theta]
    push_cast
    ring
  calc ∑ x : Fin N × Fin N × Fin N, Complex.exp ((theta N m x : ℂ) * Complex.I)
      = ∑ x : Fin N × Fin N × Fin N,
          Complex.exp
              (2 * (Real.pi : ℂ) * Complex.I * (m 0 : ℂ) * ((x.1 : ℕ) : ℂ) / (N : ℂ))
            * (Complex.exp
                (2 * (Real.pi : ℂ) * Complex.I * (m 1 : ℂ) * ((x.2.1 : ℕ) : ℂ) / (N : ℂ))
              * Complex.exp
                (2 * (Real.pi : ℂ) * Complex.I * (m 2 : ℂ) * ((x.2.2 : ℕ) : ℂ) / (N : ℂ))) :=
        Finset.sum_congr rfl fun x _ => hsplit x
    _ = (∑ j : Fin N,
            Complex.exp (2 * (Real.pi : ℂ) * Complex.I * (m 0 : ℂ) * ((j : ℕ) : ℂ) / (N : ℂ)))
          * ∑ p : Fin N × Fin N,
              Complex.exp
                  (2 * (Real.pi : ℂ) * Complex.I * (m 1 : ℂ) * ((p.1 : ℕ) : ℂ) / (N : ℂ))
                * Complex.exp
                  (2 * (Real.pi : ℂ) * Complex.I * (m 2 : ℂ) * ((p.2 : ℕ) : ℂ) / (N : ℂ)) :=
        (sum_mul_sum_prod
          (fun j : Fin N =>
            Complex.exp (2 * (Real.pi : ℂ) * Complex.I * (m 0 : ℂ) * ((j : ℕ) : ℂ) / (N : ℂ)))
          (fun p : Fin N × Fin N =>
            Complex.exp
                (2 * (Real.pi : ℂ) * Complex.I * (m 1 : ℂ) * ((p.1 : ℕ) : ℂ) / (N : ℂ))
              * Complex.exp
                (2 * (Real.pi : ℂ) * Complex.I * (m 2 : ℂ) * ((p.2 : ℕ) : ℂ) / (N : ℂ)))).symm
    _ = (∑ j : Fin N,
            Complex.exp (2 * (Real.pi : ℂ) * Complex.I * (m 0 : ℂ) * ((j : ℕ) : ℂ) / (N : ℂ)))
          * ((∑ j : Fin N,
              Complex.exp (2 * (Real.pi : ℂ) * Complex.I * (m 1 : ℂ) * ((j : ℕ) : ℂ) / (N : ℂ)))
            * (∑ j : Fin N,
              Complex.exp (2 * (Real.pi : ℂ) * Complex.I * (m 2 : ℂ) * ((j : ℕ) : ℂ) / (N : ℂ)))) := by
        rw [sum_mul_sum_prod
          (fun j : Fin N =>
            Complex.exp (2 * (Real.pi : ℂ) * Complex.I * (m 1 : ℂ) * ((j : ℕ) : ℂ) / (N : ℂ)))
          (fun j : Fin N =>
            Complex.exp (2 * (Real.pi : ℂ) * Complex.I * (m 2 : ℂ) * ((j : ℕ) : ℂ) / (N : ℂ)))]
    _ = (∑ j : Fin N,
            Complex.exp (2 * (Real.pi : ℂ) * Complex.I * (m 0 : ℂ) * ((j : ℕ) : ℂ) / (N : ℂ)))
          * (∑ j : Fin N,
            Complex.exp (2 * (Real.pi : ℂ) * Complex.I * (m 1 : ℂ) * ((j : ℕ) : ℂ) / (N : ℂ)))
          * (∑ j : Fin N,
            Complex.exp (2 * (Real.pi : ℂ) * Complex.I * (m 2 : ℂ) * ((j : ℕ) : ℂ) / (N : ℂ))) :=
        (mul_assoc _ _ _).symm
MODEL 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

The theorem does not establish the value of the continuum target, which remains open. It does not assert that any physical grid or wave exists in nature. It does not claim anything about the existence or properties of gravity itself.

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