Encyclopedia Gravity Gravity Analysis Bloch Cell Sum Cell Sum Exp Eq Prod

ARTICLE 1 claim 1 theorem

Gravity Analysis Bloch Cell Sum Cell Sum Exp Eq Prod

This lemma is a piece of classical discrete Fourier analysis: it shows that a certain three-dimensional sum of complex exponentials splits into the product of three one-dimensional sums.

Verify this page

The factorization lemma

The declaration cellSum_exp_eq_prod establishes a factorization identity in discrete Fourier analysis. It concerns a sum over a three-dimensional grid of points, where each point is indexed by three integers from 0 to N-1. At each point, the summand is a complex exponential whose phase is a linear combination of the three coordinates, with integer coefficients m0, m1, and m2. The theorem states that this three-dimensional sum equals the product of three separate one-dimensional sums, one for each coordinate. Each one-dimensional sum is the familiar geometric series of complex exponentials, summed over the N values of a single coordinate.

This is a standard result in the theory of the discrete Fourier transform on a torus. The proof in the machine-checked library of formal theorems proceeds by expanding the three-dimensional sum as a nested sum over the three coordinates, then using the fact that a sum over a product of finite sets factors into a product of sums. The factorization is a purely algebraic consequence of the exponential function's property that exp(a+b) = exp(a) * exp(b). No physics is involved in the statement or its proof.

The lemma is a building block for a larger program. The intended consumer is a computation that needs to collapse sums of products of cosines over a three-dimensional grid. The factorization lemma is the first step: it reduces the three-dimensional problem to one-dimensional sums, which are then evaluated by the classical geometric series formula. The lemma itself does not evaluate any sums; it only rearranges the three-dimensional sum into a product of one-dimensional sums.

In Recognition Science, this lemma is part of a library of formal theorems used in a campaign to analyze a continuum limit. The library is a machine-checked collection of formal theorems, and this lemma is a pure classical result with no campaign-specific axioms. It does not claim anything about the continuum limit, about the value -1/4, or about any physical quantity. Those targets remain open.

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

What this page does not claim

This lemma does not evaluate any sums, only factorizes a three-dimensional sum into one-dimensional sums. This lemma does not claim anything about the continuum limit or the value -1/4. This lemma does not involve any physics or recognition-specific axioms.

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