Encyclopedia Gravity Gravity Analysis Bloch Cell Sum Cell Sum Cos Sq Three Axis
ARTICLE 4 claims 4 theorems
Gravity Analysis Bloch Cell Sum Cell Sum Cos Sq Three Axis
A machine-checked identity shows that on a 3 by 3 by 3 grid, the sum of squared cosine values collapses to a simple fraction, a result built from classical Fourier orthogonality.
A concrete sum on a small grid
The declaration cellSum_cos_sq_three_axis is a proved identity about a finite sum of squared cosine values. It considers a three-dimensional grid of points, specifically a cube with 3 points along each axis, making 27 points in total. At each point, it evaluates the cosine of an angle that depends on the point's position along the first axis, squares that cosine, and then adds up all 27 results. The theorem states that this total is exactly 27 divided by 2.
This is not a statement about physics or gravity. It is a result in pure discrete mathematics, specifically about Fourier orthogonality on a finite grid. The angles are chosen so that the wave pattern repeats perfectly across the grid, a condition called commensurability. The proof relies on a standard identity: the product of two cosines equals half the sum of cosines of the sum and difference of their angles. When summed over the grid, the term involving the sum of angles cancels out due to orthogonality, leaving only the constant term from the difference. The result is a clean, exact number.
The identity is a concrete instance of a more general theorem. That broader result handles grids of any size and any repeating wave pattern, as long as a certain condition about the wave's frequency holds. The specific case here, with a grid of size 3 and a wave along only the first axis, provides a check that the general theorem is not vacuous. It shows the machinery works on a small, explicit example.
The declaration does not claim anything about the physical world. It does not derive a force, a particle mass, or any gravitational effect. It is a piece of mathematical infrastructure, a tool that a larger program might use to simplify sums that appear in other calculations. Its value is in being a verified, reliable building block, not in making a physical prediction.
THEOREM cellSum_cos_sq_three_axis · IndisputableMonolith/Gravity/Analysis/BlochCellSum.lean
/-- Non-vacuity witness: the headline identity engages at `N = 3`,
`m = (1, 0, 0)`, `α = β = 0`, where it evaluates the cell-sum of squared
cosines to `27 / 2`. -/
theorem cellSum_cos_sq_three_axis :
∑ x : Fin 3 × Fin 3 × Fin 3,
Real.cos (theta 3 ![1, 0, 0] x + 0) * Real.cos (theta 3 ![1, 0, 0] x + 0)
= 27 / 2 := by
haveI : NeZero (3 : ℕ) := ⟨by norm_num⟩
have halias : ∃ i : Fin 3, ¬ ((3 : ℕ) : ℤ) ∣ 2 * (![1, 0, 0] : Fin 3 → ℤ) i := by
refine ⟨0, ?_⟩
simp only [Matrix.cons_val_zero]
norm_num
have h := cellSum_cos_mul_cos 3 ![1, 0, 0] 0 0 halias
rw [h]
norm_num [sub_self, Real.cos_zero]
THEOREM cellSum_cos_sq_three_axis · IndisputableMonolith/Gravity/Analysis/BlochCellSum.lean
/-- Non-vacuity witness: the headline identity engages at `N = 3`,
`m = (1, 0, 0)`, `α = β = 0`, where it evaluates the cell-sum of squared
cosines to `27 / 2`. -/
theorem cellSum_cos_sq_three_axis :
∑ x : Fin 3 × Fin 3 × Fin 3,
Real.cos (theta 3 ![1, 0, 0] x + 0) * Real.cos (theta 3 ![1, 0, 0] x + 0)
= 27 / 2 := by
haveI : NeZero (3 : ℕ) := ⟨by norm_num⟩
have halias : ∃ i : Fin 3, ¬ ((3 : ℕ) : ℤ) ∣ 2 * (![1, 0, 0] : Fin 3 → ℤ) i := by
refine ⟨0, ?_⟩
simp only [Matrix.cons_val_zero]
norm_num
have h := cellSum_cos_mul_cos 3 ![1, 0, 0] 0 0 halias
rw [h]
norm_num [sub_self, Real.cos_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 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
This declaration does not make any statement about physics or gravity. This declaration does not derive any physical constant or force. This declaration is not a prediction that can be tested against experiment.
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:
- What is the broader theorem that this identity is an instance of?
- How does this identity get used in the larger program that needs it?
- What is the condition that must hold for the general theorem to apply?
- What is the physical or mathematical problem that motivated the need for this identity?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM cellSum_cos_sq_three_axis · IndisputableMonolith/Gravity/Analysis/BlochCellSum.lean
/-- Non-vacuity witness: the headline identity engages at `N = 3`, `m = (1, 0, 0)`, `α = β = 0`, where it evaluates the cell-sum of squared cosines to `27 / 2`. -/ theorem cellSum_cos_sq_three_axis : ∑ x : Fin 3 × Fin 3 × Fin 3, Real.cos (theta 3 ![1, 0, 0] x + 0) * Real.cos (theta 3 ![1, 0, 0] x + 0) = 27 / 2 := by haveI : NeZero (3 : ℕ) := ⟨by norm_num⟩ have halias : ∃ i : Fin 3, ¬ ((3 : ℕ) : ℤ) ∣ 2 * (![1, 0, 0] : Fin 3 → ℤ) i := by refine ⟨0, ?_⟩ simp only [Matrix.cons_val_zero] norm_num have h := cellSum_cos_mul_cos 3 ![1, 0, 0] 0 0 halias rw [h] norm_num [sub_self, Real.cos_zero]The declaration cellSum_cos_sq_three_axis is a proved identity about a finite sum of squared cosine values. cellSum_cos_sq_three_axis · IndisputableMonolith/Gravity/Analysis/BlochCellSum.leanTHEOREM cellSum_cos_sq_three_axis · IndisputableMonolith/Gravity/Analysis/BlochCellSum.lean
/-- Non-vacuity witness: the headline identity engages at `N = 3`, `m = (1, 0, 0)`, `α = β = 0`, where it evaluates the cell-sum of squared cosines to `27 / 2`. -/ theorem cellSum_cos_sq_three_axis : ∑ x : Fin 3 × Fin 3 × Fin 3, Real.cos (theta 3 ![1, 0, 0] x + 0) * Real.cos (theta 3 ![1, 0, 0] x + 0) = 27 / 2 := by haveI : NeZero (3 : ℕ) := ⟨by norm_num⟩ have halias : ∃ i : Fin 3, ¬ ((3 : ℕ) : ℤ) ∣ 2 * (![1, 0, 0] : Fin 3 → ℤ) i := by refine ⟨0, ?_⟩ simp only [Matrix.cons_val_zero] norm_num have h := cellSum_cos_mul_cos 3 ![1, 0, 0] 0 0 halias rw [h] norm_num [sub_self, Real.cos_zero]The theorem states that this total is exactly 27 divided by 2. cellSum_cos_sq_three_axis · 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]It is a result in pure discrete mathematics, specifically about Fourier orthogonality on a finite grid. 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]The identity is a concrete instance of a more general theorem. cellSum_cos_mul_cos · IndisputableMonolith/Gravity/Analysis/BlochCellSum.lean