curvatureCoupledOperator
plain-language theorem explainer
A one-parameter family of lattice operators on 3×3 tensor fields: minus the certified flat discrete Laplacian plus a zeroth-order scalar multiple of the field. Anyone building Gap-4 countermodels of curved Lichnerowicz coupling cites it. The body is a two-term pointwise definition, not a derived continuum operator.
Claim. For real parameters $c$ (coupling) and $\rho$ (curvature proxy), resolution $N\in\mathbb{N}$, and lattice tensor field $H:\mathrm{Site}_3\to M_3(\mathbb{C})$, define the operator by $(L_{c,\rho,N}H)(x)= -\Delta_3^{(N)}H(x)+(c\rho)\,H(x)$, where $\Delta_3^{(N)}$ is the componentwise 3D discrete Laplacian.
background
Gap 4 in the gravity stack is that the certified DiscreteLichnerowicz spectrum only treats axis modes of the flat lattice Laplacian. Its continuum value is definitional from the flat reduction $\Delta_L=-\Delta$; no Riemann endomorphism appears, so curvature coupling is underdetermined.
A lattice tensor field assigns a $3\times 3$ complex matrix to every site of the 3D lattice. The operator discLap3 is the componentwise sum of the three 1D second-difference stencils, scaled by $N^2$. The scalar $\rho$ here is only a curvature proxy (elsewhere in the framework $\rho=\varphi^{-1}$ is the forced per-step weight); the module uses it deliberately as a minimal stand-in, not as physical curvature.
The module constructs explicit zeroth-order curvature-coupled families that all collapse to $-\mathrm{discLap3}$ at zero curvature, yet disagree at nonzero curvature. That turns the reach gap into a theorem rather than a status flag.
proof idea
Definitional, not a proof. The operator is the pointwise sum of two scaled fields: the additive inverse of the 3D discrete Laplacian applied to $H$, plus the scalar $(c\cdot\rho)$ times $H$ itself. No lemmas are invoked; the body is a single fun x => clause using scalar multiplication on the matrix-valued field.
why it matters
This is the shared generator for the two named countermodel extensions (coupling $1$ and coupling $2$). Downstream, the flat-specialization theorem shows every member collapses to the same operator when $\rho=0$; the agreement theorem lifts that to the full single vs double pair; the distinctness theorem separates them on the constant plus-polarization whenever $\rho\neq 0$. The plane-wave theorem shows the family acts by the curved discrete eigenvalue on certified transverse axis modes.
In the Recognition gravity program this pins Gap 4: flat spectrum alone cannot identify a curved coupling. Nothing here is the physical curved Lichnerowicz operator. Closing the gap requires deriving a genuine curvature endomorphism from curved discrete geometry and proving a $C/N^2$ correction bound so SpectralConvergence can certify the continuum limit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.