cosSum_eq_zero
plain-language theorem explainer
If the period N does not divide the integer frequency a, the one-period sum of cos(2π a j/N + φ) vanishes for every real phase φ. Discrete-Fourier and Bloch-cell analysts cite this as the 1D cosine orthogonality identity on Fin N. The proof reduces the cosine sum to a geometric complex-exponential sum already known to be zero, via a casting bridge and a real-part lemma.
Claim. Let $N$ be a positive integer, $a\in\mathbb{Z}$ with $N\nmid a$, and $\varphi\in\mathbb{R}$. Then $$\sum_{j=0}^{N-1}\cos\bigl(2\pi\, a j/N+\varphi\bigr)=0.$$
background
This module records classical discrete-Fourier orthogonality on finite index cubes Fin N (and their 3D products), with Mathlib-only analysis. No Recognition-Science physics is claimed here. The intended consumer is the Regge continuum-symbol program, which sums products of cosines of commensurate Bloch phases over torus cells and needs exact closed forms.
The 1D exponential sum $\sum_{j}\exp(2\pi i a j/N)$ equals $0$ when $N\nmid a$ and equals $N$ when $N\mid a$ (geometric-series route). Cosine sums are recovered as real parts of the same roots-of-unity sums, allowing an arbitrary constant phase $\varphi$ in the argument.
Phase convention for later 3D work: cell phases are $\theta=2\pi(m\cdot x)/N$, and consumer phases arrive as $\theta+\alpha$ with constant offset $\alpha=k\cdot D/2$, so every identity is stated in the shape “linear phase plus constant.”
proof idea
One short tactic proof. Apply the sibling real-part bridge that turns a vanishing complex exponential sum into a vanishing cosine sum with additive phase $\varphi$. The remaining obligation is that $\sum_j\exp(2\pi i a j/N)=0$.
A local casting lemma equates the real-scaled form $\exp((2\pi a j/N),i)$ with the fully complex form used by the exponential-sum theorem (congruence, push_cast, ring). Finset.sum_congr transports the equality termwise, then the already-proved 1D geometric identity expSum_eq_zero (under $N\nmid a$) finishes the goal.
why it matters
This is the 1D cosine step in the Bloch cell-sum ladder. The module’s 3D factorization and vanishing results (cell exponential product, 3D cosine cell-sum zero, and the headline double-cosine cell identity) rest on reducing each coordinate sum to this statement whenever a frequency component is non-aliased.
Downstream, the ReggeTT continuum-symbol campaign needs $\sum_x\cos(\theta_m x+\alpha)\cos(\theta_m x+\beta)$ over $x\in(\mathrm{Fin},N)^3$ to collapse to $N^3\cos(\alpha-\beta)/2$ when some component of $2m$ is not divisible by $N$. That collapse is pure classical DFT; the continuum target $-1/4$ remains open and is not touched here.
Within Recognition Science this sits in the gravity/analysis support layer for discrete torus modes, not in the T0–T8 forcing chain. It supplies bookkeeping orthogonality so later continuum-symbol arguments can quote exact finite sums rather than estimates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.