Encyclopedia Gravity Gravity Analysis Bloch Cell Sum

ARTICLE 4 claims 4 theorems

Gravity Analysis Bloch Cell Sum

A trigonometric sum over a three-dimensional grid collapses to a single cosine term, a result the Recognition Science framework needs for its gravity calculations.

Verify this page

The cell-sum identity

In Recognition Science, the gravity analysis Bloch cell sum is a discrete Fourier orthogonality identity. It states that when you sum the product of two cosine waves over a three-dimensional grid of cells, the result simplifies dramatically. Specifically, for a grid with N points per side, the sum equals N cubed times the cosine of the phase difference between the two waves, divided by two. The identity holds whenever the wave's doubled frequency is not an integer multiple of N on at least one axis.

The classical mathematics here is standard. The identity is a consequence of the product-to-sum formula for cosines, combined with the fact that a geometric series of roots of unity sums to zero. The framework's machine-checked library of formal theorems proves these steps rigorously. The library contains lemmas establishing that a one-dimensional exponential sum vanishes unless its frequency is an integer multiple of N, and that the three-dimensional sum factorizes into a product of one-dimensional sums.

The framework's library then assembles these pieces into the headline result. It proves that the sum over cells of cos(θ + α) times cos(θ + β) equals N³ cos(α − β) / 2, provided the doubled frequency is non-aliased. The key step is that the product-to-sum identity splits the product into a constant term and a term at the doubled frequency. The constant term contributes the N³ cos(α − β) / 2, while the doubled-frequency term vanishes by the orthogonality lemma.

This identity is not an end in itself. The framework's gravity program needs it to collapse sums over torus cells into single cosine terms, a step in computing a continuum symbol. The module also proves that the non-aliasing condition holds for all sufficiently large N, and it provides a concrete example at N = 3 where the sum of squared cosines evaluates to 27/2. The result is purely mathematical, with no physics claims attached.

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]
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
THEOREM eventually_nonaliased · IndisputableMonolith/Gravity/Analysis/BlochCellSum.lean
eventually_nonaliased · IndisputableMonolith/Gravity/Analysis/BlochCellSum.lean:378 
/-- For a fixed nonzero frequency vector `m`, the non-aliasing hypothesis of
`cellSum_cos_mul_cos` holds for all sufficiently large `N`: once
`N > 2 * |m i|` on a nonzero axis, `N` cannot divide `2 * m i`. -/
theorem eventually_nonaliased (m : Fin 3 → ℤ) (hm : ∃ i : Fin 3, m i ≠ 0) :
    ∀ᶠ N : ℕ in Filter.atTop, ∃ i : Fin 3, ¬ (N : ℤ) ∣ 2 * m i := by
  obtain ⟨i, hi⟩ := hm
  rw [Filter.eventually_atTop]
  refine ⟨2 * (m i).natAbs + 1, fun N hN => ⟨i, fun hdvd => ?_⟩⟩
  have hne : 2 * m i ≠ 0 := mul_ne_zero two_ne_zero hi
  have hle : (N : ℤ) ≤ |2 * m i| :=
    Int.le_of_dvd (abs_pos.mpr hne) ((dvd_abs _ _).mpr hdvd)
  rw [Int.abs_eq_natAbs] at hle
  omega

What this page does not claim

This identity does not establish any physics result about gravity or the continuum target. The module does not derive the value of any physical constant. The identity is not a claim about the framework's recognition cost function.

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