Encyclopedia Gravity Gravity Analysis Bloch Cell Sum Exp Sum Eq Card

ARTICLE 3 claims 3 theorems

Gravity Analysis Bloch Cell Sum Exp Sum Eq Card

A single geometric series identity, proved for the framework's gravity calculations, that decides when a sum of equally spaced points on the unit circle cancels to zero.

Verify this page

The vanishing sum

The theorem expSum_eq_card is a statement about adding up points that sit evenly spaced around the unit circle in the complex plane. Take a whole number of steps N, and an integer frequency a. The sum in question adds up the complex numbers exp(2πI a j / N) as j runs from 0 to N-1. These are the N-th roots of unity, though possibly visited more than once if a shares a factor with N. The theorem states: if N divides a, then every term in the sum is exactly 1, so the total is simply N. This is the "aliased" case, where the frequency is a multiple of the period and the points pile onto a single location.

The complementary statement, expSum_eq_zero, covers the other case: if N does not divide a, the sum is 0. The two together form the classical discrete Fourier orthogonality relation. The proof in the machine-checked library of formal theorems runs through the geometric series formula: the ratio exp(2πI a / N) is an N-th root of unity, and when it is not 1, summing the geometric series and using that its N-th power is 1 forces the numerator to vanish. No physics enters here; this is pure algebra and analysis over the complex numbers, with no new axioms beyond the standard three.

In Recognition Science, this identity is the 1D building block for a larger calculation. The gravity program needs to sum products of cosines over a three-dimensional grid of cells, with phases coming from a wave vector k = 2π m / N. The 3D sum factorizes into three 1D sums, and the vanishing of any non-aliased axis kills the whole product. The headline result, cellSum_cos_mul_cos, uses expSum_eq_card's sibling expSum_eq_zero to collapse such a product sum to the constant N³ cos(α-β)/2. This is the tool that lets the downstream consumer replace a costly cell-by-cell summation with a single closed-form expression.

What the declaration does not claim is just as important as what it proves. It says nothing about the value of any physical quantity, and it does not touch the continuum target of -(1/4) that the broader program is chasing. That target remains OPEN. The theorem is a lemma about finite sums, not a statement about gravity itself; it is infrastructure, and the framework's honesty requires that the two layers stay distinct.

THEOREM expSum_eq_card · IndisputableMonolith/Gravity/Analysis/BlochCellSum.lean
expSum_eq_card · IndisputableMonolith/Gravity/Analysis/BlochCellSum.lean:135 
/-- 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]
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

The declaration does not assign any value to a physical constant or observable. It does not prove the continuum target of -(1/4), which remains open. It does not make any statement about the nature of gravity or spacetime.

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