singleCurvatureExtension
plain-language theorem explainer
Names the curvature-coupled lattice operator with coefficient one: flat discrete Laplacian plus a zeroth-order term ρ times the field. Gravity auditors cite it as one of two explicit countermodel extensions showing that flat spectral data do not fix curved Lichnerowicz coupling. The body is a one-line specialization of the general coupling family.
Claim. For curvature proxy $\rho\in\mathbb{R}$, resolution $N\in\mathbb{N}$, and lattice tensor field $H$ (a $3\times 3$ complex matrix at each site), the single-coefficient curved extension is $(-\mathrm{discLap}_3)_N H + \rho\, H$. Equivalently, it is the curvature-coupled family evaluated at coupling constant $1$.
background
Gap 4 in the gravity ledger concerns whether the certified flat discrete Lichnerowicz spectrum determines a curved-background coupling. The existing DiscreteLichnerowicz theorem only treats axis modes of the componentwise flat lattice Laplacian; its continuum value is the flat reduction $\Delta_L=-\Delta$, with no Riemann endomorphism.
This module builds countermodels on the actual lattice tensor-field type: maps from 3D lattice sites to $3\times 3$ complex matrices. The parent family is a one-parameter operator $H\mapsto -\mathrm{discLap}_3(N)H + (c\cdot\rho)H$, where the first term is the certified positive flat operator and the second is a scalar zeroth-order curvature proxy. The parameter $\rho$ is deliberately minimal, not a derived geometric curvature.
Two named specializations (coefficients one and two) both collapse to $-\mathrm{discLap}_3$ at $\rho=0$ for every field and resolution, yet separate on a concrete TT polarization whenever $\rho\neq 0$.
proof idea
One-line definitional wrapper: apply the general curvature-coupled operator family at coupling constant $1$. No tactics or lemmas; the meaning is inherited from that family (flat Laplacian term plus $(1\cdot\rho)$ times the field).
why it matters
This is the first of the two explicit extensions that power the Gap 4 blocker. Downstream, extensions_agree_on_entire_flat_specialization shows it coincides with the double-coefficient extension on the entire flat specialization; extensions_distinct_at_nonzero_curvature shows the operators differ at every $\rho\neq 0$; and flat_spectrum_underdetermines_curvature_coupling / gap4_curvature_coupling_blocker package both facts with matching continuum eigenvalue limits.
The FullTheoryLedger certification records that gap4_operator_recovery stays false until a genuine curvature endomorphism is derived from curved discrete geometry. Decoy-receipt theorems further show both couplings inhabit the same generic spectral-convergence predicate while remaining physically inequivalent. Nothing here claims the physical curved Lichnerowicz operator; the point is non-identifiability of the coupling from flat data alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.