discreteEigenvalue_tendsto
plain-language theorem explainer
For fixed wavenumber k, the axis-stencil discrete eigenvalue 4N² sin²(πk/N) converges to the continuum value (2πk)² as the lattice is refined. Gravity analysts cite it as the qualitative flat TT spectral limit on the unit 3-torus. The proof rewrites the eigenvalue as (2πk)² (sin x/x)² with x=πk/N→0 and uses the slope form of sin'(0)=1; the zero mode is constant zero.
Claim. For every fixed natural number $k$, the sequence $N \mapsto 4N^{2}\sin^{2}(\pi k/N)$ tends to $(2\pi k)^{2}$ in $\mathbb{R}$ as $N\to\infty$ (neighborhood filter at the limit). When $k=0$ both sides are identically zero.
background
Lane 4 of the Seven-Gaps campaign targets operator convergence: connect the discrete perturbation spectrum on a lattice to 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$, not functions on $\mathrm{ZMod},N$, so stencil identities hold pointwise and periodicity alone supplies the torus reading.
The discrete eigenvalue here is the axis-mode symbol of the spacing-normalized axis-stencil Laplacian: $4N^{2}\sin^{2}(\pi k/N)$. Upstream in the same module, Fourier modes $\exp(2\pi i k j/N)$ are shown to be eigenvectors of that stencil, so the scalar sequence is the genuine eigenvalue along $k=(k,0,0)$.
Scope is deliberately axis-sector only. Test G (Freudenthal stencil preflight / energy limit) established that the continuum moment tensor of the frozen quadratic energy is anisotropic, $A_{0}=(1+\sqrt{2})I+(\sqrt{2}+\sqrt{3})J$; axis stencils cannot see body-diagonal stiffness. Direction-resolved symbol recovery is deferred to the C10 probe.
proof idea
Case split on $k$. If $k=0$, discreteEigenvalue N 0 is identically $0$ by direct unfolding, the continuum target is $0$, and constant sequences tend to their value.
If $k>0$, start from $\mathrm{HasDerivAt},\sin,0$ (so $\cos 0=1$) and pass to the slope characterization: $\sin y/y\to 1$ along $\mathcal{N}[\neq]0$. The argument $x_{N}=\pi k/N$ tends to $0$ by constant-over-$N$, and for $N\ge 1$ it stays strictly positive, hence lands in the punctured neighborhood. Compose to get $\sin x_{N}/x_{N}\to 1$, square, and multiply by the constant $(2\pi k)^{2}$. A final eventual congruence (field simplification and ring) identifies that product with discreteEigenvalue N k for $N\ge 1$.
why it matters
This is the core qualitative convergence theorem of DiscreteLichnerowicz and the first genuine Lean bridge from discrete lattice eigenvalues to continuum Lichnerowicz on flat $T^{3}$. Downstream, discrete_eigenvalue_tendsto_raw is the campaign-brief spelling (same statement, unfolded formula), and discrete_tt_spectrum_converges_to_flat_lichnerowicz packages the spectral claim.
Quantitative rate work in SpectralConvergence.discrete_sine_eigenvalue_expansion cites it as the qualitative limit behind the $O(1/N^{2})$ bound $|4N^{2}\sin^{2}(\pi k/N)-(2\pi k)^{2}|\le(2\pi k)^{4}/(12N^{2})$. Curved countermodels build on it directly: curvedDiscreteEigenvalue_tendsto is flat convergence plus a constant curvature shift, and the blocker curvedSpectrumConverges_iff_curvatureCorrectionConsistent records that flat convergence alone cannot discharge curved targets without an independent curvature-correction premise. The campaign ledger anchors Gap-4 flags against this artifact so booleans cannot drift.
Within RS gravity, it closes the flat axis-sector half of the operator-convergence gap; isotropic full-symbol recovery and curved consistency remain open under C10/C14.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.