cellSum_cos_eq_zero
plain-language theorem explainer
On the N×N×N torus cell, the sum of cos(θ_m(x)+φ) vanishes whenever some integer frequency component m_i is not divisible by N, for any constant phase φ. Discrete-Fourier / Bloch consumers in the Regge continuum-symbol program cite it to kill the doubled-frequency half of a product-to-sum identity. The proof reduces the cosine sum to a factorized complex exponential product and applies the 1D geometric vanishing lemma on the non-aliased axis.
Claim. Let $N\ge 1$ and $m:\{0,1,2\}\to\mathbb{Z}$. Write $\theta_N(m,x)=2\pi(m_0 x_0+m_1 x_1+m_2 x_2)/N$ for $x\in(\mathbb{Z}/N\mathbb{Z})^3$. If some component satisfies $N\nmid m_i$, then for every real phase $\varphi$, $\sum_x \cos(\theta_N(m,x)+\varphi)=0$.
background
This module records classical Bloch / discrete-Fourier orthogonality on finite torus cells Fin N × Fin N × Fin N, Mathlib-only, with no physics claims. The phase convention is fixed: theta N m x = 2π (m·x)/N with each coordinate the underlying natural of the Fin N index. Downstream consumers receive phases as k·(x+D/2) = theta + constant, so every identity is stated as theta plus a constant phase.
The 1D building block is the geometric exponential sum: if N does not divide the integer frequency a, then ∑_{j:Fin N} exp(2π I a j / N) = 0 (expSum_eq_zero), proved from the geometric series with ratio ≠ 1 whose N-th power is 1. The 3D cell exponential sum factorizes into the product of three such 1D sums (cellSum_exp_eq_prod). A private real-part extraction lemma then converts a vanishing complex exponential sum into a vanishing cosine sum with arbitrary phase offset (sum_cos_of_sum_exp_eq_zero).
proof idea
One-step reduction via sum_cos_of_sum_exp_eq_zero: it suffices that the complex cell sum ∑_x exp(I · theta N m x) vanish. Rewrite that sum by cellSum_exp_eq_prod as the product of three 1D geometric sums. Unpack the hypothesis that some axis i is non-aliased (N ∤ m i), then fin_cases on i. On each branch, expSum_eq_zero kills the corresponding 1D factor, and mul_eq_zero_of_left / mul_eq_zero_of_right push the zero through the product.
why it matters
This is the vanishing half of the module's headline identity cellSum_cos_mul_cos: for non-aliased doubled frequency ∃ i, N ∤ 2 m i, the cell sum of cos(theta+α) cos(theta+β) equals N³ cos(α-β)/2. The product-to-sum split (cos_mul_cos) contributes a constant (A-B) term and a doubled-frequency (A+B) cell-sum; the latter is killed exactly by applying this theorem at frequency 2m. The intended consumer is the ReggeTTContinuumSymbol program (QG full-theory campaign, Crux-1c), which needs these classical Bloch collapses on torus cells. The module explicitly leaves the continuum -(1/4) target OPEN; nothing here closes that gap. Framework-wise this is pure discrete analysis scaffolding for gravity continuum symbols, not a T0–T8 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.