doubleCurvatureExtension
plain-language theorem explainer
Names the second explicit curvature-coupled lattice operator family, with fixed coefficient two on the curvature proxy. Gravity and spectral-geometry workers cite it as one of the two countermodel extensions that agree on every flat specialization yet separate at nonzero curvature. The body is a one-line specialization of the general curvature-coupled operator at coefficient 2.
Claim. For a real curvature proxy $\rho$, resolution $N\in\mathbb{N}$, and lattice tensor field $H$, the double curvature extension is the curvature-coupled discrete operator with coefficient $2$: $\mathrm{Op}_{2,\rho,N}(H)$.
background
Gap 4 in the gravity ledger is that the certified DiscreteLichnerowicz spectrum theorem only treats axis modes of the componentwise flat lattice Laplacian. Its continuum value is definitional from the flat reduction $\Delta_L=-\Delta$; no Riemann-curvature endomorphism appears, so the flat theorem cannot fix a curved-background coupling.
This module exhibits that underdetermination on the actual lattice tensor-field type. A general curvature-coupled operator adds a zeroth-order term scaled by a coefficient times a scalar curvature proxy $\rho$. The single extension uses coefficient one; the double extension uses coefficient two. Both reduce to $-\mathrm{discLap}_3$ at $\rho=0$ for every field and resolution.
The scalar $\rho$ is deliberately minimal, not the physical curvature endomorphism. The module's second half isolates the missing analytic premise: curved eigenvalue convergence is equivalent to convergence of the curvature correction relative to the certified flat value, with a $C/N^2$ bound as a sufficient certificate.
proof idea
One-line definitional wrapper: instantiate the general curvature-coupled operator at coefficient $2$, passing through the curvature proxy $\rho$, resolution $N$, and lattice tensor field $H$. No further proof obligations.
why it matters
This is the second named countermodel in the Gap 4 curvature-coupling blocker. Downstream, extensions_agree_on_entire_flat_specialization shows the single and double extensions coincide for every field when $\rho=0$; extensions_distinct_at_nonzero_curvature shows they differ at every $\rho\neq 0$, witnessed by a constant-plus-polarization field on which the flat Laplacian vanishes while the two coefficients act by $\rho$ and $2\rho$.
Those facts package into flat_spectrum_underdetermines_curvature_coupling and the final gap4_curvature_coupling_blocker, which the FullTheoryLedger certifies so that gap4_operator_recovery stays false until a genuine curved coupling is derived. The Gap4OperatorDecoyReceipt uses both extensions as inhabited countermodels of CurvedSpectrumConverges: both eigenvalue branches converge, but to distinct curved continuum values. Nothing here claims the physical Lichnerowicz operator; it only proves the existing flat spectrum plus generic rate-bound machinery does not determine the coupling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.