CurvedSpectrumConverges
plain-language theorem explainer
Defines the Gap 4 target property: a discrete curved eigenvalue family converges, at every curvature proxy and wavenumber, to a proposed continuum curved spectrum. Gravity and spectral-geometry workers cite it when stating curved Lichnerowicz consistency without committing to a physical coupling. It is a pure Prop abbreviation of pointwise Filter.Tendsto as mesh goes to infinity.
Claim. A pair of maps $(d, c)$, with $d(\rho, N, k)$ the discrete curved eigenvalue at curvature proxy $\rho$, resolution $N$, and mode $k$, and $c(\rho, k)$ the proposed continuum value, is said to have curved spectral convergence when for every $\rho$ and $k$, $d(\rho, N, k) \to c(\rho, k)$ as $N \to \infty$.
background
Gap 4 in the SevenGaps gravity stack records that the certified discrete spectrum theorem (axis modes of the componentwise flat lattice Laplacian in DiscreteLichnerowicz) never sees a Riemann-curvature endomorphism. Its continuum target is definitional from the flat reduction $\Delta_L = -\Delta$, so it cannot fix a curved-background coupling.
This module exhibits the underdetermination explicitly: two zeroth-order curvature-coupled operator families both specialize to $-\mathrm{discLap}_3$ at zero curvature, yet disagree on a concrete nonzero TT polarization at every nonzero curvature. Both branches still obey the flat theorem and both admit continuum limits, with different curved limits. The scalar $\rho$ is only a minimal curvature proxy used to show non-identifiability, not the physical curvature endomorphism.
Relative to the flat convergence theorem, full curved convergence is equivalent to convergence of the curvature correction (curved value minus certified flat value). A quantitative $C/N^2$ correction bound is a sufficient certificate via the spectral-analysis eigenvalue-limit lemma.
proof idea
Definitional Prop, not a proved theorem. The body is the universal quantification over curvature proxy $\rho$ and wavenumber $k$ of the statement that the $N$-sequence of discrete curved eigenvalues tends, in the filter-at-top sense, to the neighborhood filter of the proposed continuum curved eigenvalue. No lemmas are applied; the name packages that Tendsto shape for later iff and rate theorems.
why it matters
This is the Gap 4 target shape kept separate from the missing analytic premise. Downstream, curvedSpectrumConverges_iff_curvatureCorrectionConsistent is the blocker: because the flat branch already converges, full curved convergence is equivalent to convergence of precisely the omitted curvature correction, so the flat theorem cannot discharge the curved target alone. curvedSpectrumConverges_of_correctionRateBound packages the constructive direction: a proved correction-rate bound plus flat convergence yields this property.
Gap4OperatorDecoyReceipt uses it as the inhabited false path: both free scalar couplings (one and two) satisfy the property via curvedDiscreteEigenvalue_tendsto, yet remain physically inequivalent at every nonzero curvature. The headline receipt curvedSpectrumConverges_inhabited_by_countermodels records that inhabitation without uniqueness. Closing Gap 4 still requires deriving the genuine curvature endomorphism from curved discrete geometry and proving its correction consistent with continuum Riemann coupling; nothing here defines that physical operator.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.