fourierMode
plain-language theorem explainer
Defines the standard complex Fourier mode of integer wavenumber k on an N-site lattice: the map j ↦ exp(2π i k j / N) from ℤ to ℂ. Anyone proving discrete Laplacian eigenvalues or building axis plane waves on the flat 3-torus cites this. The body is a direct noncomputable exponential formula, not a derived identity.
Claim. For $N \in \mathbb{N}$ and wavenumber $k \in \mathbb{Z}$, the Fourier mode is the function $j \mapsto \exp(2\pi i\, k j / N)$ from $\mathbb{Z}$ to $\mathbb{C}$.
background
The 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 a flat 3-torus. Lattice functions are represented as $N$-periodic maps $\mathbb{Z} \to \mathbb{C}$ (spacing $h = 1/N$ on the unit circle), not as functions on $\mathrm{ZMod}, N$, so stencil identities hold pointwise for every $j \in \mathbb{Z}$ and periodicity alone grounds the torus reading.
All convergence results here are axis-sector only: plane waves $k = (k,0,0)$ under the componentwise axis-stencil Laplacian. The Freudenthal frozen quadratic energy has an anisotropic continuum moment tensor, so axis stencils do not recover an isotropic full Lichnerowicz spectrum.
The discrete Laplacian and its eigenvalue calculus act on these modes; one-step shifts multiply by $\exp(\pm i\theta)$ with $\theta = 2\pi k/N$, which feeds the half-angle identity $2\cos\theta - 2 = -4\sin^2(\theta/2)$.
proof idea
Pure definition: the body is the pointwise complex exponential
$j \mapsto \exp\bigl(2\pi i, k j / N\bigr)$
with the usual coercions of $k$, $j$, and $N$ into $\mathbb{C}$. No lemmas are applied; downstream lemmas unfold this definition and use Complex.exp_add for shifts.
why it matters
This is the elementary spectral atom for the discrete Lichnerowicz file. Downstream, fourierMode_periodic shows it lives on the $N$-site circle; fourierMode_step and fourierMode_step_down give the $\pm 1$ multiplications by $\exp(\pm i\theta)$; and discLap_fourierMode_apply / discLap_fourierMode prove the eigenvalue identity
$\mathrm{discLap},(\mathrm{mode}) = -\bigl(4 N^2 \sin^2(\pi k/N)\bigr),\mathrm{mode}$.
The 3D axis plane wave planeH is exactly this 1D mode in the first coordinate times a constant polarization matrix, so the whole axis-sector spectrum pipeline rests on the definition. In the Recognition gravity stack it is the lattice-side input to continuum Lichnerowicz convergence on $T^3$, not a claim about full isotropic recovery (that remains under the C10 / P-iso probe).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.