discLap3_planeH
plain-language theorem explainer
The axis plane-wave tensor field on the flat 3-torus lattice is an eigenvector of the componentwise 3D discrete Laplacian, with the same eigenvalue as the 1D Fourier mode: −4 N² sin²(π k/N). Anyone assembling the discrete TT spectrum package cites this identity. The proof reduces componentwise to the 1D eigenvalue formula, since the y- and z-stencils act trivially on a mode constant in those directions.
Claim. For every lattice size $N\in\mathbb{N}$, wavenumber $k\in\mathbb{Z}$, constant polarization matrix $\varepsilon\in M_3(\mathbb{C})$, and site $x\in\mathbb{Z}^3$, the 3D discrete Laplacian of the axis plane wave $H(x)=\varepsilon\,e^{2\pi i k x_1/N}$ satisfies $\Delta_3 H(x)=\bigl(-4 N^2\sin^2(\pi k/N)\bigr) H(x)$.
background
This module sits in the Seven-Gaps campaign, Lane 4 (operator convergence), and builds the first Lean link between the discrete perturbation spectrum on a lattice and the continuum Lichnerowicz operator on the flat 3-torus. Lattice functions are N-periodic maps $\mathbb{Z}\to\mathbb{C}$ with spacing $h=1/N$; 3D sites are Site3 $:=\mathbb{Z}^3$ with axis periodicity.
The 1D spacing-normalized discrete Laplacian is $(\mathrm{discLap},N,f)(j)=N^2\bigl(f(j+1)-2f(j)+f(j-1)\bigr)$. Its 3D lift discLap3 sums the three axis stencils componentwise on a lattice tensor field (a $3\times 3$ complex matrix at each site). The axis plane wave planeH N k ε is the rank-2 field constant in $y,z$ and modulated by the 1D Fourier mode $e^{2\pi i k x_1/N}$ in the first coordinate, with fixed polarization $\varepsilon$.
Upstream, discLap_fourierMode_apply already gives the pointwise 1D identity: the mode is an eigenvector with scalar $-4 N^2\sin^2(\pi k/N)$, via $f(j\pm 1)=f(j)e^{\pm i\theta}$ and $2\cos\theta-2=-4\sin^2(\theta/2)$.
proof idea
Componentwise extensionality on the $3\times 3$ matrix entries. Unfold discLap3 and the plane-wave definition; the six neighbor shifts simplify via the fst_add_e* / fst_sub_e* lemmas so that only the $x_1$-direction moves the phase, while $y$- and $z$-neighbors leave the first coordinate fixed. The resulting 1D stencil expression is exactly discLap on the Fourier mode at $x_1$. Invoke discLap_fourierMode_apply and finish by linear_combination against the polarization entry $\varepsilon_{ij}$.
why it matters
This is the exact eigenvector half of the discrete TT package. Downstream, discrete_tt_spectrum_converges_to_flat_lichnerowicz quotes it for every resolution $N$: the axis plane wave is discrete-transverse and an eigenvector of discLap3 with eigenvalue $-(\mathrm{discreteEigenvalue},N,k)$, which then tends to the continuum flat Lichnerowicz symbol. Without the 3D identity matching the 1D eigenvalue, the spectrum-convergence claim has no discrete eigenbasis to pass to the limit.
Scope is deliberately axis-sector only (panel mandate C14). Axis stencils are blind to the Freudenthal anisotropy $A_0=(1+\sqrt{2})I+(\sqrt{2}+\sqrt{3})J$; this lemma does not claim isotropic flat-space recovery of the full Lichnerowicz spectrum. Direction-resolved symbols remain under the C10 probe. In the broader Recognition gravity lane it closes the discrete-to-continuum operator step on the flat background before curved or anisotropic extensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.