CurvatureCorrectionConsistent
plain-language theorem explainer
Names the missing analytic premise for curved spectral limits: the discrete curvature correction (curved eigenvalue minus the certified flat lattice eigenvalue) must converge to the continuum curvature correction as resolution N goes to infinity. Spectral-geometry and RS gravity workers cite it to separate flat Lichnerowicz control from genuine curvature coupling. It is a Prop definition packaging a Tendsto statement, not a proved claim.
Claim. A pair of families $E^{\mathrm{d}}(\rho,N,k)$ (discrete curved eigenvalues) and $E^{\mathrm{c}}(\rho,k)$ (continuum curved eigenvalues) is curvature-correction consistent when, for every curvature proxy $\rho\in\mathbb{R}$ and wavenumber $k\in\mathbb{N}$, $$\lim_{N\to\infty}\bigl(E^{\mathrm{d}}(\rho,N,k)-4N^{2}\sin^{2}(\pi k/N)\bigr)=E^{\mathrm{c}}(\rho,k)-(2\pi k)^{2}.$$
background
Gap 4 in the gravity stack: the certified spectrum theorem in DiscreteLichnerowicz only treats axis modes of the componentwise flat lattice Laplacian. Its continuum value is introduced from the flat reduction $\Delta_L=-\Delta$; it carries no Riemann-curvature endomorphism and cannot fix a curved-background coupling.
The module builds two explicit zeroth-order curvature-coupled operator families on the lattice tensor-field type. Both reduce to the same $-\mathrm{discLap3}$ at zero curvature for every field and resolution, yet they disagree on a concrete nonzero TT polarization at every nonzero curvature. Both branches satisfy the flat theorem and have certified continuum limits, with different curved limits.
Flat baselines used here: discrete eigenvalue $4N^{2}\sin^{2}(\pi k/N)$, continuum flat Lichnerowicz value $(2\pi k)^{2}$. The scalar $\rho$ is a deliberately minimal curvature proxy for non-identifiability, not the physical curved operator.
proof idea
Definitional Prop with no proof body. It asserts that for all curvature proxies $\rho$ and modes $k$, the map $N\mapsto E^{\mathrm{d}}(\rho,N,k)-4N^{2}\sin^{2}(\pi k/N)$ tends at infinity to the neighborhood filter of $E^{\mathrm{c}}(\rho,k)-(2\pi k)^{2}$. The subtracted terms are exactly the certified flat discrete and continuum eigenvalues from DiscreteLichnerowicz, so the Prop isolates only the curvature correction omitted by the flat theorem.
why it matters
Parent results use it as the exact missing premise. The blocker equivalence states that, because the flat branch already converges, full curved spectral convergence is equivalent to this correction consistency; the flat theorem alone cannot discharge a curved target. A companion theorem shows a quantitative $C/N^{2}$ bound on the correction is a sufficient certificate, via the spectral-convergence toolkit (uniform bound implies eigenvalue limit).
In the Recognition gravity program this turns a status gap into a named analytic obligation: any candidate curved discrete operator must prove its correction converges to the continuum Riemann coupling. Closing Gap 4 still requires deriving that genuine curvature endomorphism from curved discrete geometry; nothing here supplies the physical Lichnerowicz operator on a curved background.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.