expSum_eq_zero
plain-language theorem explainer
When the integer frequency a is not a multiple of the period N, the discrete Fourier sum of exp(2π i a j / N) over one full period vanishes. Discrete-analysis and lattice-gravity consumers cite this as the non-aliased 1D geometric sum. The proof rewrites each term as a power of the unit ratio, applies the closed geometric-sum formula, and uses that the ratio is an N-th root of unity different from 1.
Claim. Let $N\ge 1$ and $a\in\mathbb{Z}$. If $N\nmid a$, then $$\sum_{j=0}^{N-1}\exp\bigl(2\pi i\, a j/N\bigr)=0.$$
background
The module develops classical Bloch cell-sum orthogonality on finite torus cells Fin N (and products thereof). It is pure discrete Fourier analysis: Mathlib-only algebra and complex analysis, with no physics hypotheses. The intended consumer is the ReggeTT continuum-symbol program, which collapses 3D cell-sums of products of cosines of commensurate phases theta N m x = 2π (m·x)/N.
The 1D building block is the geometric exponential sum with unit ratio r = exp(2π i a / N). Upstream, exp_ratio_pow_card shows r^N = 1 for every integer frequency a (so r is always an N-th root of unity, primitive or not). The companion exp_ratio_eq_one_iff characterizes the aliased case: r = 1 if and only if N divides a. Each summand is identified with a power of r by exp_term_eq_pow.
This theorem treats the non-aliased case ¬ N ∣ a. The aliased twin (expSum_eq_card) asserts the complementary identity that the sum equals N when every summand is 1.
proof idea
First obtain r ≠ 1 from the hypothesis ¬ N ∣ a via exp_ratio_eq_one_iff. Rewrite the Fin-sum by exp_term_eq_pow so each summand is r^(j : ℕ), then transport to Finset.range N by Fin.sum_univ_eq_sum_range. Apply Mathlib's geom_sum_eq (valid because r ≠ 1) to get (r^N - 1)/(r - 1). Finally exp_ratio_pow_card gives r^N = 1, so the numerator vanishes and the quotient is 0.
why it matters
This is the non-aliased half of the 1D geometric exponential sum that the module lists as its first content item. Downstream, cosSum_eq_zero lifts it to cosine phase sums with arbitrary constant phase φ (via the real-part bridge sum_cos_of_sum_exp_eq_zero). The 3D vanishing theorem cellSum_cos_eq_zero then factorizes the cell exponential sum into a product of three 1D sums and kills the product whenever some component frequency is non-aliased.
Those identities feed the headline cell-sum cellSum_cos_mul_cos, which supplies the exact value needed by ReggeTTContinuumSymbol (QG Crux-1c) when the doubled wave-vector 2m is non-aliased. The module explicitly leaves the continuum target -(1/4) open; nothing here closes that gap. The result is classical DFT orthogonality, not an RS forcing-chain step (T0–T8), but it is the analytic engine for the gravity-side Bloch reduction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.