fourierMode_step
plain-language theorem explainer
On the N-site discrete circle, shifting a Fourier mode of wavenumber k by one lattice site multiplies it by exp(2π i k/N). Anyone deriving the discrete Laplacian eigenvalue on plane waves cites this one-step cocycle identity. The proof unfolds the exponential definition and collapses the phase additivity by ring arithmetic.
Claim. For every lattice size $N\in\mathbb{N}$, wavenumber $k\in\mathbb{Z}$, and site $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)\cdot\exp(2\pi i 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 on $\mathbb{Z}$.
The Fourier mode is defined by $f_{N,k}(j)=\exp(2\pi i k j/N)$. Periodicity of these modes grounds the torus interpretation. The one-step shift identity is the elementary cocycle that turns neighbor evaluations $f(j\pm 1)$ into multiplications by pure phases $\exp(\pm i\theta)$ with $\theta=2\pi k/N$, which is the algebraic input to the discrete eigenvalue calculation.
proof idea
Unfold fourierMode at $j+1$ and at $j$. Rewrite the product of the mode value and the phase factor via Complex.exp_add (run backwards), so both sides become a single exponential. Congruence on the exponent, followed by push_cast and ring, equates the linear forms $2\pi i k(j+1)/N$ and $2\pi i k j/N + 2\pi i k/N$. No external lemmas beyond the definition and complex exponential additivity are required.
why it matters
Parent use is discLap_fourierMode_apply, the pointwise eigenvalue identity: the spacing-normalized discrete Laplacian multiplies the Fourier mode by $-(4N^2\sin^2(\pi k/N))$ at every site. That theorem's derivation explicitly invokes this step (and the matching down-shift) to replace $f(j\pm 1)$ by $f(j)\exp(\pm i\theta)$, then uses $e^{i\theta}+e^{-i\theta}=2\cos\theta$ and the half-angle identity $2\cos\theta-2=-4\sin^2(\theta/2)$.
In the Recognition gravity stack this is scaffolding for discrete-to-continuum spectral convergence of the Lichnerowicz operator on $T^3$, not a continuum GR claim. Scope remains the axis sector only; isotropic full-symbol recovery is deferred to the C10 probe. The lemma itself is pure Fourier arithmetic on the circle and does not touch the forcing chain (T0–T8) or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.