curvedDiscreteEigenvalue_tendsto
plain-language theorem explainer
Each scalar-curvature countermodel eigenvalue branch converges in the continuum limit. Gravity auditors cite it when packaging Gap 4 underdetermination: two curved operator extensions share the certified flat spectrum yet both admit continuum limits. The proof is a one-line sum of the existing flat discrete-eigenvalue Tendsto with constant-neighborhood convergence of the curvature correction.
Claim. For every real coupling $c$, curvature proxy $\rho$, and mode index $k\in\mathbb{N}$, the sequence $N\mapsto \lambda_N^{\mathrm{flat}}(k)+c\rho$ tends to $\lambda^{\mathrm{flat}}(k)+c\rho$ in the filter topology as lattice resolution $N\to\infty$.
background
Gap 4 records that the certified spectrum theorem in DiscreteLichnerowicz only treats axis modes of the componentwise flat lattice Laplacian. Its continuum value is definitional from the flat reduction $\Delta_L=-\Delta$; it carries no Riemann-curvature endomorphism and cannot fix a curved-background coupling.
This module builds two explicit zeroth-order curvature-coupled operator families on the lattice tensor-field type. Both reduce to $-\mathrm{discLap}_3$ at zero curvature for every field and resolution, yet they separate on a concrete nonzero TT polarization whenever curvature is nonzero. The scalar parameter $\rho$ is a minimal curvature proxy used only to exhibit non-identifiability.
The discrete curved eigenvalue is the certified flat discrete eigenvalue plus the constant $c\rho$; the continuum curved value is the certified flat Lichnerowicz eigenvalue plus the same constant. Upstream, the flat discrete branch already converges to the flat continuum value.
proof idea
One-line term proof. Apply the certified flat result discreteEigenvalue_tendsto at mode $k$, then add tendsto_const_nhds for the constant curvature correction $c\rho$. Filter arithmetic for sums closes the claim: flat Tendsto plus constant Tendsto yields Tendsto of the curved branch to the curved continuum value.
why it matters
This is the convergence half of the Gap 4 underdetermination package. Downstream, flat_spectrum_underdetermines_curvature_coupling uses it to show two extensions agree on the entire flat specialization, separate at every nonzero curvature, and both eigenvalue branches converge to distinct curved limits. The Gap 4 decoy receipts wrap it as curvedSpectrumConverges_of_coupling and the coupling-2 inhabitant of CurvedSpectrumConverges.
In the Recognition gravity stack this turns a status flag into a theorem: flat spectral data alone cannot select a curvature coupling. It does not close Gap 4. The module doc states the missing premise explicitly: a genuine curved discrete geometry must supply the Riemann endomorphism and a quantitative $C/N^2$ correction bound via the spectral-convergence certificate. Until that construction exists, every free scalar coupling remains a certified false path.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.