IndisputableMonolith.Gravity.Analysis.BlochCellSum
IndisputableMonolith/Gravity/Analysis/BlochCellSum.lean · 416 lines · 16 declarations
show as:
view math explainer →
1import Mathlib
2
3/-!
4# Bloch cell-sum orthogonality identities (discrete Fourier, torus cells)
5
6Status: THEOREM (pure classical discrete Fourier orthogonality on `Fin N`
7index cubes; Mathlib-only analysis and algebra, no campaign imports, no
8physics claims).
9
10## Intended consumer
11
12The `ReggeTTContinuumSymbol` program (QG full-theory campaign, Crux-1c)
13needs the classical Bloch orthogonality identities to collapse torus
14cell-sums of products of cosines into single cosines of phase differences.
15The downstream consumer sums, over cells `x : Fin N × Fin N × Fin N`,
16terms `cos (θ_m x + α) * cos (θ_m x + β)` with commensurate wave vector
17`k = 2 π m / N` (`m : Fin 3 → ℤ` fixed), and needs the exact value
18`N ^ 3 * cos (α - β) / 2` whenever the doubled frequency `2 m` is
19non-aliased, i.e. some component of `2 m` is not divisible by `N`.
20Nothing here touches the `-(1/4)` continuum target, which remains OPEN.
21
22## Phase convention (read before consuming)
23
24`theta N m x = 2 * π * (m 0 * x₀ + m 1 * x₁ + m 2 * x₂ : ℤ) / N` with
25`x = (x₀, (x₁, x₂))` and each `xᵢ` the underlying natural number of the
26`Fin N` component. The consumer's phases arrive as
27`k · (x + D/2) = theta N m x + α` with the constant `α = k · D / 2`, so
28every statement below is shaped as `theta + constant phase`.
29
30## Contents
31
32* `expSum_eq_zero` / `expSum_eq_card`: the 1D geometric exponential sum
33 `∑ j : Fin N, exp (2 π I a j / N)` equals `0` when `¬ (N : ℤ) ∣ a` and
34 equals `N` when `(N : ℤ) ∣ a`. Proved from `geom_sum_eq` (no suitable
35 ready-made root-of-unity sum exists in Mathlib for non-primitive
36 integer frequencies, so the geometric-series route is used).
37* `cosSum_eq_zero`: the 1D cosine phase sum
38 `∑ j : Fin N, cos (2 π a j / N + φ) = 0` for `¬ (N : ℤ) ∣ a`, any `φ`.
39* `cellSum_exp_eq_prod`: the 3D cell exponential sum factorizes into the
40 product of three 1D sums.
41* `cellSum_cos_eq_zero`: the 3D cosine cell-sum vanishes whenever some
42 component frequency is non-aliased.
43* `cellSum_cos_mul_cos` (HEADLINE): for `∃ i, ¬ (N : ℤ) ∣ 2 * m i`,
44 `∑ x, cos (theta N m x + α) * cos (theta N m x + β)
45 = N ^ 3 * cos (α - β) / 2`.
46* `eventually_nonaliased`: for fixed `m ≠ 0` the non-aliasing hypothesis
47 holds for all sufficiently large `N`.
48* `cellSum_cos_sq_three_axis`: concrete non-vacuity instance at `N = 3`,
49 `m = (1, 0, 0)`, `α = β = 0`, evaluating to `27 / 2`.
50
51No `sorry`, no `admit`, no new axioms, no `native_decide`. Expected
52axiom footprint: the standard trio (propext, Classical.choice, Quot.sound).
53-/
54
55namespace IndisputableMonolith
56namespace Gravity
57namespace Analysis
58namespace BlochCellSum
59
60open scoped BigOperators
61
62noncomputable section
63
64/-! ## 1D building blocks -/
65
66/-- The unit ratio `exp (2 π I a / N)` raised to the `N`-th power is `1`
67(the ratio is always an `N`-th root of unity, primitive or not). -/
68lemma exp_ratio_pow_card (N : ℕ) [NeZero N] (a : ℤ) :
69 Complex.exp (2 * (Real.pi : ℂ) * Complex.I * (a : ℂ) / (N : ℂ)) ^ N = 1 := by
70 have hN : (N : ℂ) ≠ 0 := Nat.cast_ne_zero.mpr (NeZero.ne N)
71 rw [← Complex.exp_nat_mul]
72 have harg : (N : ℂ) * (2 * (Real.pi : ℂ) * Complex.I * (a : ℂ) / (N : ℂ))
73 = (a : ℂ) * (2 * (Real.pi : ℂ) * Complex.I) := by
74 rw [mul_comm ((N : ℂ)) (2 * (Real.pi : ℂ) * Complex.I * (a : ℂ) / (N : ℂ)),
75 div_mul_cancel₀ _ hN]
76 ring
77 rw [harg]
78 exact Complex.exp_int_mul_two_pi_mul_I a
79
80/-- The ratio `exp (2 π I a / N)` equals `1` exactly when `N` divides the
81integer frequency `a`. -/
82lemma exp_ratio_eq_one_iff (N : ℕ) [NeZero N] (a : ℤ) :
83 Complex.exp (2 * (Real.pi : ℂ) * Complex.I * (a : ℂ) / (N : ℂ)) = 1
84 ↔ (N : ℤ) ∣ a := by
85 have hN : (N : ℂ) ≠ 0 := Nat.cast_ne_zero.mpr (NeZero.ne N)
86 rw [Complex.exp_eq_one_iff]
87 constructor
88 · rintro ⟨n, hn⟩
89 refine ⟨n, ?_⟩
90 have h2 : 2 * (Real.pi : ℂ) * Complex.I * (a : ℂ)
91 = (n : ℂ) * (2 * (Real.pi : ℂ) * Complex.I) * (N : ℂ) := (div_eq_iff hN).mp hn
92 have h3 : (a : ℂ) * (2 * (Real.pi : ℂ) * Complex.I)
93 = ((n : ℂ) * (N : ℂ)) * (2 * (Real.pi : ℂ) * Complex.I) := by
94 linear_combination h2
95 have key : (a : ℂ) = (n : ℂ) * (N : ℂ) :=
96 mul_right_cancel₀ Complex.two_pi_I_ne_zero h3
97 exact_mod_cast key.trans (mul_comm (n : ℂ) ((N : ℕ) : ℂ))
98 · rintro ⟨n, rfl⟩
99 refine ⟨n, ?_⟩
100 rw [div_eq_iff hN]
101 push_cast
102 ring
103
104/-- Each 1D summand is a power of the unit ratio. -/
105lemma exp_term_eq_pow (N : ℕ) [NeZero N] (a : ℤ) (j : Fin N) :
106 Complex.exp (2 * (Real.pi : ℂ) * Complex.I * (a : ℂ) * ((j : ℕ) : ℂ) / (N : ℂ))
107 = Complex.exp (2 * (Real.pi : ℂ) * Complex.I * (a : ℂ) / (N : ℂ)) ^ (j : ℕ) := by
108 rw [← Complex.exp_nat_mul]
109 congr 1
110 ring
111
112/-- GEOMETRIC EXPONENTIAL SUM, non-aliased case: if `N` does not divide the
113integer frequency `a`, the sum of `exp (2 π I a j / N)` over one period
114vanishes. Geometric series with ratio `≠ 1` whose `N`-th power is `1`. -/
115theorem expSum_eq_zero (N : ℕ) [NeZero N] (a : ℤ) (ha : ¬ (N : ℤ) ∣ a) :
116 ∑ j : Fin N,
117 Complex.exp (2 * (Real.pi : ℂ) * Complex.I * (a : ℂ) * ((j : ℕ) : ℂ) / (N : ℂ))
118 = 0 := by
119 have hr_ne : Complex.exp (2 * (Real.pi : ℂ) * Complex.I * (a : ℂ) / (N : ℂ)) ≠ 1 :=
120 fun h => ha ((exp_ratio_eq_one_iff N a).mp h)
121 calc ∑ j : Fin N,
122 Complex.exp (2 * (Real.pi : ℂ) * Complex.I * (a : ℂ) * ((j : ℕ) : ℂ) / (N : ℂ))
123 = ∑ j : Fin N,
124 Complex.exp (2 * (Real.pi : ℂ) * Complex.I * (a : ℂ) / (N : ℂ)) ^ (j : ℕ) :=
125 Finset.sum_congr rfl fun j _ => exp_term_eq_pow N a j
126 _ = ∑ j ∈ Finset.range N,
127 Complex.exp (2 * (Real.pi : ℂ) * Complex.I * (a : ℂ) / (N : ℂ)) ^ j :=
128 Fin.sum_univ_eq_sum_range
129 (fun k => Complex.exp (2 * (Real.pi : ℂ) * Complex.I * (a : ℂ) / (N : ℂ)) ^ k) N
130 _ = (Complex.exp (2 * (Real.pi : ℂ) * Complex.I * (a : ℂ) / (N : ℂ)) ^ N - 1)
131 / (Complex.exp (2 * (Real.pi : ℂ) * Complex.I * (a : ℂ) / (N : ℂ)) - 1) :=
132 geom_sum_eq hr_ne N
133 _ = 0 := by rw [exp_ratio_pow_card N a, sub_self, zero_div]
134
135/-- GEOMETRIC EXPONENTIAL SUM, aliased case: if `N` divides the integer
136frequency `a`, every summand is `1` and the sum equals `N`. -/
137theorem expSum_eq_card (N : ℕ) [NeZero N] (a : ℤ) (ha : (N : ℤ) ∣ a) :
138 ∑ j : Fin N,
139 Complex.exp (2 * (Real.pi : ℂ) * Complex.I * (a : ℂ) * ((j : ℕ) : ℂ) / (N : ℂ))
140 = (N : ℂ) := by
141 obtain ⟨c, rfl⟩ := ha
142 have hN : (N : ℂ) ≠ 0 := Nat.cast_ne_zero.mpr (NeZero.ne N)
143 have hterm : ∀ j : Fin N,
144 Complex.exp
145 (2 * (Real.pi : ℂ) * Complex.I * (((N : ℤ) * c : ℤ) : ℂ) * ((j : ℕ) : ℂ) / (N : ℂ))
146 = 1 := by
147 intro j
148 have harg :
149 2 * (Real.pi : ℂ) * Complex.I * (((N : ℤ) * c : ℤ) : ℂ) * ((j : ℕ) : ℂ) / (N : ℂ)
150 = ((c * (j : ℕ) : ℤ) : ℂ) * (2 * (Real.pi : ℂ) * Complex.I) := by
151 rw [div_eq_iff hN]
152 push_cast
153 ring
154 rw [harg]
155 exact Complex.exp_int_mul_two_pi_mul_I _
156 calc ∑ j : Fin N,
157 Complex.exp
158 (2 * (Real.pi : ℂ) * Complex.I * (((N : ℤ) * c : ℤ) : ℂ) * ((j : ℕ) : ℂ) / (N : ℂ))
159 = ∑ _j : Fin N, (1 : ℂ) := Finset.sum_congr rfl fun j _ => hterm j
160 _ = (N : ℂ) := by
161 simp only [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul, mul_one]
162
163/-! ## Real-part transfer: complex sum zero forces cosine sum zero -/
164
165/-- If the complex exponential sum of phases `θf` vanishes, then the cosine
166sum with any constant phase offset `φ` vanishes. This is the real-part
167extraction `cos (θ + φ) = re (exp (θ I) * exp (φ I))` summed. -/
168private lemma sum_cos_of_sum_exp_eq_zero {ι : Type*} [Fintype ι] (θf : ι → ℝ) (φ : ℝ)
169 (hz : ∑ x : ι, Complex.exp ((θf x : ℂ) * Complex.I) = 0) :
170 ∑ x : ι, Real.cos (θf x + φ) = 0 := by
171 have hterm : ∀ x : ι,
172 Real.cos (θf x + φ)
173 = (Complex.exp ((θf x : ℂ) * Complex.I)
174 * Complex.exp ((φ : ℂ) * Complex.I)).re := by
175 intro x
176 rw [← Complex.exp_add]
177 have harg : (θf x : ℂ) * Complex.I + (φ : ℂ) * Complex.I
178 = ((θf x + φ : ℝ) : ℂ) * Complex.I := by
179 push_cast
180 ring
181 rw [harg, Complex.exp_ofReal_mul_I_re]
182 calc ∑ x : ι, Real.cos (θf x + φ)
183 = ∑ x : ι,
184 (Complex.exp ((θf x : ℂ) * Complex.I) * Complex.exp ((φ : ℂ) * Complex.I)).re :=
185 Finset.sum_congr rfl fun x _ => hterm x
186 _ = ((∑ x : ι, Complex.exp ((θf x : ℂ) * Complex.I))
187 * Complex.exp ((φ : ℂ) * Complex.I)).re := by
188 rw [Finset.sum_mul, Complex.re_sum]
189 _ = 0 := by rw [hz, zero_mul, Complex.zero_re]
190
191/-- COSINE PHASE SUM (1D): if `N` does not divide the integer frequency `a`,
192the cosine sum over one period vanishes for every constant phase `φ`. -/
193theorem cosSum_eq_zero (N : ℕ) [NeZero N] (a : ℤ) (ha : ¬ (N : ℤ) ∣ a) (φ : ℝ) :
194 ∑ j : Fin N,
195 Real.cos (2 * Real.pi * (a : ℝ) * ((j : ℕ) : ℝ) / (N : ℝ) + φ) = 0 := by
196 refine sum_cos_of_sum_exp_eq_zero
197 (fun j : Fin N => 2 * Real.pi * (a : ℝ) * ((j : ℕ) : ℝ) / (N : ℝ)) φ ?_
198 have hbridge : ∀ j : Fin N,
199 Complex.exp (((2 * Real.pi * (a : ℝ) * ((j : ℕ) : ℝ) / (N : ℝ) : ℝ)) * Complex.I : ℂ)
200 = Complex.exp
201 (2 * (Real.pi : ℂ) * Complex.I * (a : ℂ) * ((j : ℕ) : ℂ) / (N : ℂ)) := by
202 intro j
203 congr 1
204 push_cast
205 ring
206 exact (Finset.sum_congr rfl fun j _ => hbridge j).trans (expSum_eq_zero N a ha)
207
208/-! ## 3D torus cell phases -/
209
210/-- Cell phase for the commensurate wave vector `k = 2 π m / N` at cell
211`x = (x₀, (x₁, x₂))`:
212`theta N m x = 2 π (m 0 * x₀ + m 1 * x₁ + m 2 * x₂) / N`.
213The consumer's phases arrive as `k · (x + D/2) = theta N m x + α` with the
214constant `α = k · D / 2`, so all statements below take the shape
215`theta + constant phase`. -/
216def theta (N : ℕ) (m : Fin 3 → ℤ) (x : Fin N × Fin N × Fin N) : ℝ :=
217 2 * Real.pi
218 * ((m 0 * ((x.1 : ℕ) : ℤ) + m 1 * ((x.2.1 : ℕ) : ℤ) + m 2 * ((x.2.2 : ℕ) : ℤ) : ℤ) : ℝ)
219 / (N : ℝ)
220
221/-- Doubling every component of the frequency vector doubles the cell phase. -/
222lemma theta_two_mul (N : ℕ) (m : Fin 3 → ℤ) (x : Fin N × Fin N × Fin N) :
223 theta N (fun i => 2 * m i) x = 2 * theta N m x := by
224 simp only [theta]
225 push_cast
226 ring
227
228/-- Product sums factor through the product type (helper for the 3D
229factorization). -/
230private lemma sum_mul_sum_prod {ι κ : Type*} [Fintype ι] [Fintype κ]
231 (u : ι → ℂ) (v : κ → ℂ) :
232 (∑ j : ι, u j) * (∑ k : κ, v k) = ∑ p : ι × κ, u p.1 * v p.2 := by
233 rw [Finset.sum_mul_sum]
234 exact (Fintype.sum_prod_type fun p : ι × κ => u p.1 * v p.2).symm
235
236/-- The 3D cell exponential sum factorizes into the product of the three 1D
237geometric exponential sums (one per axis). -/
238theorem cellSum_exp_eq_prod (N : ℕ) [NeZero N] (m : Fin 3 → ℤ) :
239 ∑ x : Fin N × Fin N × Fin N, Complex.exp ((theta N m x : ℂ) * Complex.I)
240 = (∑ j : Fin N,
241 Complex.exp (2 * (Real.pi : ℂ) * Complex.I * (m 0 : ℂ) * ((j : ℕ) : ℂ) / (N : ℂ)))
242 * (∑ j : Fin N,
243 Complex.exp (2 * (Real.pi : ℂ) * Complex.I * (m 1 : ℂ) * ((j : ℕ) : ℂ) / (N : ℂ)))
244 * (∑ j : Fin N,
245 Complex.exp (2 * (Real.pi : ℂ) * Complex.I * (m 2 : ℂ) * ((j : ℕ) : ℂ) / (N : ℂ))) := by
246 have hsplit : ∀ x : Fin N × Fin N × Fin N,
247 Complex.exp ((theta N m x : ℂ) * Complex.I)
248 = Complex.exp
249 (2 * (Real.pi : ℂ) * Complex.I * (m 0 : ℂ) * ((x.1 : ℕ) : ℂ) / (N : ℂ))
250 * (Complex.exp
251 (2 * (Real.pi : ℂ) * Complex.I * (m 1 : ℂ) * ((x.2.1 : ℕ) : ℂ) / (N : ℂ))
252 * Complex.exp
253 (2 * (Real.pi : ℂ) * Complex.I * (m 2 : ℂ) * ((x.2.2 : ℕ) : ℂ) / (N : ℂ))) := by
254 intro x
255 rw [← Complex.exp_add, ← Complex.exp_add]
256 congr 1
257 simp only [theta]
258 push_cast
259 ring
260 calc ∑ x : Fin N × Fin N × Fin N, Complex.exp ((theta N m x : ℂ) * Complex.I)
261 = ∑ x : Fin N × Fin N × Fin N,
262 Complex.exp
263 (2 * (Real.pi : ℂ) * Complex.I * (m 0 : ℂ) * ((x.1 : ℕ) : ℂ) / (N : ℂ))
264 * (Complex.exp
265 (2 * (Real.pi : ℂ) * Complex.I * (m 1 : ℂ) * ((x.2.1 : ℕ) : ℂ) / (N : ℂ))
266 * Complex.exp
267 (2 * (Real.pi : ℂ) * Complex.I * (m 2 : ℂ) * ((x.2.2 : ℕ) : ℂ) / (N : ℂ))) :=
268 Finset.sum_congr rfl fun x _ => hsplit x
269 _ = (∑ j : Fin N,
270 Complex.exp (2 * (Real.pi : ℂ) * Complex.I * (m 0 : ℂ) * ((j : ℕ) : ℂ) / (N : ℂ)))
271 * ∑ p : Fin N × Fin N,
272 Complex.exp
273 (2 * (Real.pi : ℂ) * Complex.I * (m 1 : ℂ) * ((p.1 : ℕ) : ℂ) / (N : ℂ))
274 * Complex.exp
275 (2 * (Real.pi : ℂ) * Complex.I * (m 2 : ℂ) * ((p.2 : ℕ) : ℂ) / (N : ℂ)) :=
276 (sum_mul_sum_prod
277 (fun j : Fin N =>
278 Complex.exp (2 * (Real.pi : ℂ) * Complex.I * (m 0 : ℂ) * ((j : ℕ) : ℂ) / (N : ℂ)))
279 (fun p : Fin N × Fin N =>
280 Complex.exp
281 (2 * (Real.pi : ℂ) * Complex.I * (m 1 : ℂ) * ((p.1 : ℕ) : ℂ) / (N : ℂ))
282 * Complex.exp
283 (2 * (Real.pi : ℂ) * Complex.I * (m 2 : ℂ) * ((p.2 : ℕ) : ℂ) / (N : ℂ)))).symm
284 _ = (∑ j : Fin N,
285 Complex.exp (2 * (Real.pi : ℂ) * Complex.I * (m 0 : ℂ) * ((j : ℕ) : ℂ) / (N : ℂ)))
286 * ((∑ j : Fin N,
287 Complex.exp (2 * (Real.pi : ℂ) * Complex.I * (m 1 : ℂ) * ((j : ℕ) : ℂ) / (N : ℂ)))
288 * (∑ j : Fin N,
289 Complex.exp (2 * (Real.pi : ℂ) * Complex.I * (m 2 : ℂ) * ((j : ℕ) : ℂ) / (N : ℂ)))) := by
290 rw [sum_mul_sum_prod
291 (fun j : Fin N =>
292 Complex.exp (2 * (Real.pi : ℂ) * Complex.I * (m 1 : ℂ) * ((j : ℕ) : ℂ) / (N : ℂ)))
293 (fun j : Fin N =>
294 Complex.exp (2 * (Real.pi : ℂ) * Complex.I * (m 2 : ℂ) * ((j : ℕ) : ℂ) / (N : ℂ)))]
295 _ = (∑ j : Fin N,
296 Complex.exp (2 * (Real.pi : ℂ) * Complex.I * (m 0 : ℂ) * ((j : ℕ) : ℂ) / (N : ℂ)))
297 * (∑ j : Fin N,
298 Complex.exp (2 * (Real.pi : ℂ) * Complex.I * (m 1 : ℂ) * ((j : ℕ) : ℂ) / (N : ℂ)))
299 * (∑ j : Fin N,
300 Complex.exp (2 * (Real.pi : ℂ) * Complex.I * (m 2 : ℂ) * ((j : ℕ) : ℂ) / (N : ℂ))) :=
301 (mul_assoc _ _ _).symm
302
303/-- 3D COSINE CELL-SUM VANISHING: if some component frequency `m i` is not
304divisible by `N`, the cosine cell-sum with any constant phase `φ` vanishes.
305The 3D exponential sum factorizes and the non-aliased axis kills the
306product. -/
307theorem cellSum_cos_eq_zero (N : ℕ) [NeZero N] (m : Fin 3 → ℤ)
308 (h : ∃ i : Fin 3, ¬ (N : ℤ) ∣ m i) (φ : ℝ) :
309 ∑ x : Fin N × Fin N × Fin N, Real.cos (theta N m x + φ) = 0 := by
310 refine sum_cos_of_sum_exp_eq_zero (theta N m) φ ?_
311 rw [cellSum_exp_eq_prod N m]
312 obtain ⟨i, hi⟩ := h
313 fin_cases i
314 · exact mul_eq_zero_of_left (mul_eq_zero_of_left (expSum_eq_zero N (m 0) hi) _) _
315 · exact mul_eq_zero_of_left (mul_eq_zero_of_right _ (expSum_eq_zero N (m 1) hi)) _
316 · exact mul_eq_zero_of_right _ (expSum_eq_zero N (m 2) hi)
317
318/-! ## Product-to-sum assembly (headline) -/
319
320/-- Product-to-sum identity for cosines, stated for reuse by consumers. -/
321theorem cos_mul_cos (A B : ℝ) :
322 Real.cos A * Real.cos B = (Real.cos (A - B) + Real.cos (A + B)) / 2 := by
323 rw [Real.cos_sub, Real.cos_add]
324 ring
325
326/-- HEADLINE (PRODUCT-TO-SUM BLOCH CELL SUM): for a commensurate wave vector
327`k = 2 π m / N` whose doubled frequency `2 m` is non-aliased on some axis
328(`∃ i, ¬ (N : ℤ) ∣ 2 * m i`), the torus cell-sum of the product of two
329phase-shifted cosines collapses to the constant term:
330`∑ x, cos (theta N m x + α) * cos (theta N m x + β) = N ^ 3 * cos (α - β) / 2`.
331The `(A - B)` half of the product-to-sum identity is constant and
332contributes `N ^ 3 * cos (α - β) / 2`; the `(A + B)` half is a cell-sum at
333doubled frequency and vanishes by `cellSum_cos_eq_zero`. -/
334theorem cellSum_cos_mul_cos (N : ℕ) [NeZero N] (m : Fin 3 → ℤ) (α β : ℝ)
335 (halias : ∃ i : Fin 3, ¬ (N : ℤ) ∣ 2 * m i) :
336 ∑ x : Fin N × Fin N × Fin N,
337 Real.cos (theta N m x + α) * Real.cos (theta N m x + β)
338 = (N : ℝ) ^ 3 * Real.cos (α - β) / 2 := by
339 have hzero :
340 ∑ x : Fin N × Fin N × Fin N,
341 Real.cos (theta N (fun i => 2 * m i) x + (α + β)) = 0 :=
342 cellSum_cos_eq_zero N (fun i => 2 * m i) halias (α + β)
343 have hpt : ∀ x : Fin N × Fin N × Fin N,
344 Real.cos (theta N m x + α) * Real.cos (theta N m x + β)
345 = Real.cos (α - β) / 2
346 + Real.cos (theta N (fun i => 2 * m i) x + (α + β)) / 2 := by
347 intro x
348 rw [cos_mul_cos]
349 rw [show theta N m x + α - (theta N m x + β) = α - β from by ring]
350 rw [show theta N m x + α + (theta N m x + β) = 2 * theta N m x + (α + β) from by ring]
351 rw [← theta_two_mul N m x]
352 ring
353 calc ∑ x : Fin N × Fin N × Fin N,
354 Real.cos (theta N m x + α) * Real.cos (theta N m x + β)
355 = ∑ x : Fin N × Fin N × Fin N,
356 (Real.cos (α - β) / 2
357 + Real.cos (theta N (fun i => 2 * m i) x + (α + β)) / 2) :=
358 Finset.sum_congr rfl fun x _ => hpt x
359 _ = (∑ _x : Fin N × Fin N × Fin N, Real.cos (α - β) / 2)
360 + ∑ x : Fin N × Fin N × Fin N,
361 Real.cos (theta N (fun i => 2 * m i) x + (α + β)) / 2 :=
362 Finset.sum_add_distrib
363 _ = (N : ℝ) ^ 3 * Real.cos (α - β) / 2 := by
364 have hconst : (∑ _x : Fin N × Fin N × Fin N, Real.cos (α - β) / 2)
365 = (N : ℝ) ^ 3 * Real.cos (α - β) / 2 := by
366 simp only [Finset.sum_const, Finset.card_univ, Fintype.card_prod,
367 Fintype.card_fin, nsmul_eq_mul]
368 push_cast
369 ring
370 have hosc : (∑ x : Fin N × Fin N × Fin N,
371 Real.cos (theta N (fun i => 2 * m i) x + (α + β)) / 2) = 0 := by
372 simp only [div_eq_mul_inv, ← Finset.sum_mul]
373 rw [hzero, zero_mul]
374 rw [hconst, hosc, add_zero]
375
376/-! ## Eventual non-aliasing -/
377
378/-- For a fixed nonzero frequency vector `m`, the non-aliasing hypothesis of
379`cellSum_cos_mul_cos` holds for all sufficiently large `N`: once
380`N > 2 * |m i|` on a nonzero axis, `N` cannot divide `2 * m i`. -/
381theorem eventually_nonaliased (m : Fin 3 → ℤ) (hm : ∃ i : Fin 3, m i ≠ 0) :
382 ∀ᶠ N : ℕ in Filter.atTop, ∃ i : Fin 3, ¬ (N : ℤ) ∣ 2 * m i := by
383 obtain ⟨i, hi⟩ := hm
384 rw [Filter.eventually_atTop]
385 refine ⟨2 * (m i).natAbs + 1, fun N hN => ⟨i, fun hdvd => ?_⟩⟩
386 have hne : 2 * m i ≠ 0 := mul_ne_zero two_ne_zero hi
387 have hle : (N : ℤ) ≤ |2 * m i| :=
388 Int.le_of_dvd (abs_pos.mpr hne) ((dvd_abs _ _).mpr hdvd)
389 rw [Int.abs_eq_natAbs] at hle
390 omega
391
392/-! ## Concrete non-vacuity instance -/
393
394/-- Non-vacuity witness: the headline identity engages at `N = 3`,
395`m = (1, 0, 0)`, `α = β = 0`, where it evaluates the cell-sum of squared
396cosines to `27 / 2`. -/
397theorem cellSum_cos_sq_three_axis :
398 ∑ x : Fin 3 × Fin 3 × Fin 3,
399 Real.cos (theta 3 ![1, 0, 0] x + 0) * Real.cos (theta 3 ![1, 0, 0] x + 0)
400 = 27 / 2 := by
401 haveI : NeZero (3 : ℕ) := ⟨by norm_num⟩
402 have halias : ∃ i : Fin 3, ¬ ((3 : ℕ) : ℤ) ∣ 2 * (![1, 0, 0] : Fin 3 → ℤ) i := by
403 refine ⟨0, ?_⟩
404 simp only [Matrix.cons_val_zero]
405 norm_num
406 have h := cellSum_cos_mul_cos 3 ![1, 0, 0] 0 0 halias
407 rw [h]
408 norm_num [sub_self, Real.cos_zero]
409
410end
411
412end BlochCellSum
413end Analysis
414end Gravity
415end IndisputableMonolith
416