discLap
plain-language theorem explainer
Spacing-normalized 1D discrete Laplacian on an N-site circle: at site j it returns N² times the second difference f(j+1)−2f(j)+f(j−1), i.e. the stencil divided by h² with h=1/N. Anyone proving discrete-to-continuum spectral convergence for the flat-torus Lichnerowicz operator cites this operator. The body is a one-line pointwise formula, not a proof.
Claim. For $N\in\mathbb{N}$ and $f:\mathbb{Z}\to\mathbb{C}$, the spacing-normalized discrete Laplacian is $(\Delta_N f)(j)=N^2\bigl(f(j+1)-2f(j)+f(j-1)\bigr)$, equivalently $(f(j+1)-2f(j)+f(j-1))/h^2$ with lattice spacing $h=1/N$ on the unit circle.
background
The module sits in the Seven-Gaps campaign, Lane 4 (operator convergence). It builds the first Lean link between the discrete perturbation spectrum on a lattice and the continuum Lichnerowicz operator, restricted to the flat 3-torus. Lattice functions are N-periodic maps $\mathbb{Z}\to\mathbb{C}$ (period $N$, spacing $h=1/N$), not functions on $\mathrm{ZMod},N$, so stencil identities hold pointwise for every $j\in\mathbb{Z}$ and periodicity of Fourier modes grounds the torus reading.
The continuum target is the Lichnerowicz operator on metric perturbations. Convergence results in this file are axis-sector only: plane waves $k=(k,0,0)$ under the componentwise axis-stencil Laplacian. Axis stencils are blind to the known anisotropy of the Freudenthal frozen quadratic energy, so these identities are not isotropic flat-space recovery of the full spectrum.
This definition is the 1D building block. The 3D axis operator is assembled from three copies of it; Fourier modes $j\mapsto\exp(2\pi i k j/N)$ are the eigenfunctions used downstream.
proof idea
Pure definition: no tactics. The map sends $f$ to the function $j\mapsto N^2\bigl(f(j+1)-2f(j)+f(j-1)\bigr)$. The factor $N^2=1/h^2$ is the standard spacing normalization that makes the discrete second difference converge to $\partial_{xx}$ as $N\to\infty$. Noncomputable only because the codomain is $\mathbb{C}$.
why it matters
This operator is the 1D stencil underlying the discrete Lichnerowicz spectrum on the flat torus. Downstream, discLap_fourierMode_apply and discLap_fourierMode prove the eigenvalue identity $\Delta_N e^{2\pi i k\cdot/N}=-(4N^2\sin^2(\pi k/N)),e^{2\pi i k\cdot/N}$ pointwise and as functions. That scalar is the discrete symbol whose $N\to\infty$ limit recovers the continuum Laplacian eigenvalue on the circle.
The 3D lift discLap3_planeH reuses the same eigenvalue for axis plane waves: $y,z$ stencils act trivially on modes constant in those directions. Together these close the first genuine discrete-to-continuum spectral step in Lane 4, still restricted to the axis sector. They do not yet address the direction-resolved symbol or isotropic recovery flagged by the C10/C14 panel notes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.