Encyclopedia Gravity Gravity Analysis Bloch Cell Sum Cell Sum Cos Mul Cos
ARTICLE 4 claims 4 theorems
Gravity Analysis Bloch Cell Sum Cell Sum Cos Mul Cos
A machine-checked theorem showing that certain sums of products of cosine waves on a discrete three-dimensional torus collapse to a single constant term.
A trigonometric identity on a discrete torus
In classical Fourier analysis, summing a product of two cosine waves over a full period often produces a simple result because the oscillating parts cancel. The theorem cellSum_cos_mul_cos establishes the exact discrete analogue on a three-dimensional torus of N cells per side. For a wave vector whose doubled frequency is not an integer multiple of N on at least one axis, the sum over all N³ cells of the product of two cosines with phase offsets α and β equals exactly N³ times the cosine of the phase difference (α − β), divided by 2. This is a pure statement about discrete Fourier orthogonality, proved in the machine-checked library of formal theorems with no unverified assumptions.
The identity is the discrete version of the familiar continuous fact that the integral of cos(A)cos(B) over a full period vanishes unless the frequencies match. Here, the product-to-sum formula rewrites the product as a sum of cosines of the sum and difference of the phases. The difference term is constant across the torus and contributes the main result. The sum term oscillates at the doubled frequency and vanishes by a separate orthogonality theorem, provided the doubled frequency is not aliased, meaning it does not wrap around the discrete grid. The theorem also shows that for any fixed nonzero frequency vector, this non-aliasing condition holds for all sufficiently large N, so the simplification applies in the large-grid limit.
The result is a building block for a larger program that studies gravitational theories on discrete spacetime cells. The program needs this identity to collapse sums over torus cells into single cosine terms, which simplifies the analysis of a continuum limit. The theorem itself, however, makes no statement about gravity, physics, or any continuum limit. It is a classical result in discrete Fourier analysis, and the framework's library proves it using only the standard axioms of the ambient type theory.
What the theorem does not claim is as precise as what it proves. It does not establish the value of any continuum integral, and it does not apply when the doubled frequency is aliased on every axis. It also makes no claim about the physical content of the program that consumes it. The identity is a standalone mathematical fact, available to any consumer who needs to simplify sums of products of cosine waves on a discrete torus.
THEOREM cellSum_cos_mul_cos · IndisputableMonolith/Gravity/Analysis/BlochCellSum.lean
/-- 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 cellSum_cos_mul_cos · IndisputableMonolith/Gravity/Analysis/BlochCellSum.lean
/-- 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 eventually_nonaliased · IndisputableMonolith/Gravity/Analysis/BlochCellSum.lean
/-- 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
THEOREM cellSum_cos_mul_cos · IndisputableMonolith/Gravity/Analysis/BlochCellSum.lean
/-- 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 prove any result about the continuum limit or about gravity itself. The theorem does not apply when the doubled frequency is aliased on every axis. The theorem does not establish the value of any integral over a continuous space.
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:
- How does this discrete orthogonality identity help in taking a continuum limit in the gravitational program?
- What is the physical interpretation of the phase difference α − β in the consumer's context?
- What happens to the sum when the doubled frequency is aliased on every axis?
- What other discrete orthogonality identities does the framework's library provide for torus cell sums?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM cellSum_cos_mul_cos · IndisputableMonolith/Gravity/Analysis/BlochCellSum.lean
/-- 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]The theorem cellSum_cos_mul_cos establishes the exact discrete analogue on a three-dimensional torus of N cells per side. cellSum_cos_mul_cos · IndisputableMonolith/Gravity/Analysis/BlochCellSum.leanTHEOREM cellSum_cos_mul_cos · IndisputableMonolith/Gravity/Analysis/BlochCellSum.lean
/-- 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]For a wave vector whose doubled frequency is not an integer multiple of N on at least one axis, the sum over all N³ cells of the product of two cosines with phase offsets α and β equals exactly N³ times the cosine of the phase difference (α − β), divided by 2. cellSum_cos_mul_cos · IndisputableMonolith/Gravity/Analysis/BlochCellSum.leanTHEOREM eventually_nonaliased · IndisputableMonolith/Gravity/Analysis/BlochCellSum.lean
/-- 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 omegaThe theorem also shows that for any fixed nonzero frequency vector, this non-aliasing condition holds for all sufficiently large N. eventually_nonaliased · IndisputableMonolith/Gravity/Analysis/BlochCellSum.leanTHEOREM cellSum_cos_mul_cos · IndisputableMonolith/Gravity/Analysis/BlochCellSum.lean
/-- 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]The theorem itself, however, makes no statement about gravity, physics, or any continuum limit. cellSum_cos_mul_cos · IndisputableMonolith/Gravity/Analysis/BlochCellSum.lean