curvedContinuumEigenvalues_distinct
plain-language theorem explainer
At every nonzero curvature proxy ρ and every mode index k, the continuum eigenvalues of the two curvature-coupled operator extensions disagree. Gravity and spectral-geometry workers cite this as the continuum half of the Gap 4 underdetermination package: flat data alone cannot select a curved coupling. The proof is a short term argument: unfold the continuum eigenvalue definition and contradict ρ ≠ 0 by linear arithmetic.
Claim. For every real curvature proxy $\rho \neq 0$ and every natural number $k$, the continuum eigenvalue attached to the first curvature-coupled extension at $(\rho,k)$ is unequal to the continuum eigenvalue attached to the second extension at the same $(\rho,k)$.
background
Gap 4 in the gravity stack records that the certified discrete Lichnerowicz spectrum only treats axis modes of the componentwise flat lattice Laplacian. Its continuum value is introduced definitionally from the flat reduction $\Delta_L = -\Delta$, with no Riemann-curvature endomorphism, so it cannot fix a curved-background coupling.
This module exhibits the gap as a theorem. On the lattice tensor-field type it builds two explicit zeroth-order curvature-coupled operator families. Both reduce to the same $-\mathrm{discLap}_3$ at zero curvature for every field and resolution, yet they separate on a concrete nonzero TT polarization whenever the scalar curvature proxy $\rho$ is nonzero. Each family has a discrete eigenvalue branch and a continuum limit value curvedContinuumEigenvalue indexed by extension label (1 or 2), $\rho$, and mode $k$.
The parameter $\rho$ is deliberately minimal: a scalar stand-in used only to witness non-identifiability, not the physical curved Lichnerowicz endomorphism.
proof idea
Term-mode proof by contradiction. Assume the two continuum values at extension labels 1 and 2 agree for the given $\rho$ and $k$. Unfold the definition of the continuum eigenvalue at that hypothesis; the unfolded equality forces a linear relation that holds only if $\rho = 0$. Discharge with linarith against the hypothesis $\rho \neq 0$. No external lemmas are invoked; the separation is definitional once the two curved continuum formulas are expanded.
why it matters
Together with the discrete separation and the two certified continuum limits, this theorem closes the continuum half of the module's underdetermination package: the same full flat operator data admits two extensions that agree everywhere at zero curvature, both of whose eigenvalue branches converge, yet the curved continuum targets remain distinct at every $\rho \neq 0$.
That package turns Gap 4 from a status flag into a proved obstruction. Anyone claiming that the existing flat spectrum theorem already determines curvature coupling must confront this pair of limits. The module is explicit that nothing here is the physical curved Lichnerowicz operator; a closing Gap 4 construction must still derive the genuine curvature endomorphism from curved discrete geometry and prove its correction consistent with continuum Riemann coupling (via a quantitative $C/N^2$ bound and eigenvalue_limit_of_uniform_bound).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.