fourierMode_step_down
plain-language theorem explainer
On the N-site discrete circle, shifting a Fourier mode of wavenumber k one site left multiplies it by exp(-iθ) with θ = 2πk/N. Anyone deriving the discrete Laplacian eigenvalue on plane waves needs this companion to the up-shift identity. The proof unfolds the exponential definition, uses exp-add, and finishes by ring on the phase.
Claim. For $N \in \mathbb{N}$ and $k,j \in \mathbb{Z}$, the Fourier mode $f_{N,k}(j) = \exp(2\pi i k j / N)$ satisfies $f_{N,k}(j-1) = f_{N,k}(j)\,\exp(-i\theta)$ where $\theta = 2\pi k/N$.
background
This module sits in the Seven-Gaps campaign, Lane 4 (operator convergence). It connects the discrete perturbation spectrum on a lattice to the continuum Lichnerowicz operator on the flat 3-torus, restricted to the axis stencil sector: plane waves $k=(k,0,0)$ under the componentwise axis Laplacian. Lattice functions are $N$-periodic maps $\mathbb{Z}\to\mathbb{C}$ with spacing $h=1/N$, not functions on $\mathrm{ZMod},N$, so stencil identities hold pointwise for every $j\in\mathbb{Z}$.
The Fourier mode of wavenumber $k$ is $j\mapsto\exp(2\pi i k j/N)$. The companion one-step up-shift multiplies by $\exp(+i\theta)$; this lemma is the down-shift. Together they feed the discrete Laplacian stencil $f(j+1)+f(j-1)-2f(j)$, which becomes the eigenvalue identity after the cosine double-angle reduction.
proof idea
Term-mode algebraic identity. Unfold fourierMode at $j-1$ and $j$. Rewrite the product of exponentials via Complex.exp_add (in reverse), so both sides are a single exponential. Congruence on the exponent, then push_cast and ring equate the phases: the $j-1$ phase is the $j$ phase plus $-2\pi i k/N$.
why it matters
Parent consumer is discLap_fourierMode_apply: the pointwise eigenvalue identity that the discrete Laplacian acts on the Fourier mode by the scalar $-(4N^2\sin^2(\pi k/N))$ at every lattice site. That theorem explicitly invokes both the up-shift and this down-shift, then uses $\exp(i\theta)+\exp(-i\theta)=2\cos\theta$ and $2\cos\theta-2=-4\sin^2(\theta/2)$.
In the Recognition gravity stack this is scaffolding for discrete-to-continuum spectrum convergence on the flat torus (axis sector only). It does not touch the forcing chain T0–T8 or the J-cost directly; it is pure lattice harmonic analysis needed before any continuum Lichnerowicz limit. Axis stencils remain blind to Freudenthal anisotropy, so isotropic full-spectrum recovery is out of scope here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.