constantPlusField
plain-language theorem explainer
Defines the spatially constant plus-polarized lattice tensor field: every site carries the matrix diag(0,1,-1). It is the explicit witness that two curvature-coupled discrete operators agree on the flat specialization yet differ at nonzero curvature. Anyone citing the Gap 4 underdetermination argument uses this field. The body is a one-line constant function into the plus polarization.
Claim. Let $\varepsilon_+$ denote the plus polarization $\mathrm{diag}(0,1,-1)$ on $\mathbb{C}^{3\times 3}$. The constant plus field is the lattice tensor field $x\mapsto\varepsilon_+$ on every site of the $3$-torus lattice.
background
Gap 4 in the gravity stack records that the certified discrete Lichnerowicz spectrum only treats axis modes of the componentwise flat lattice Laplacian. That operator has no Riemann endomorphism, so its spectrum cannot fix a curved-background coupling. This module exhibits the obstruction: two explicit zeroth-order curvature-coupled families both reduce to $-\mathrm{discLap}_3$ at zero curvature, yet disagree on a concrete TT polarization whenever the curvature proxy $\rho$ is nonzero.
A lattice tensor field is a map from lattice sites to $3\times 3$ complex matrices. The plus polarization $\varepsilon_+$ is the fixed matrix $\mathrm{diag}(0,1,-1)$; the cross polarization is the companion $E_{23}+E_{32}$. The constant plus field is the simplest nonzero TT-type configuration: the same $\varepsilon_+$ at every site. Because it is spatially constant, the flat discrete Laplacian annihilates it, so any difference between the two curved extensions is pure curvature coupling.
proof idea
Pure definition: the field is the constant function sending every lattice site to $\varepsilon_+$. No lemmas are applied; the type is the lattice tensor-field abbreviation $\mathrm{Site}3\to\mathrm{Mat}{3\times 3}(\mathbb{C})$.
why it matters
This field is the concrete witness for Gap 4 underdetermination. Downstream, discLap3_constantPlusField_zero proves the flat lattice Laplacian kills it, so the flat specialization of either curvature extension vanishes on it. Then extensions_distinct_at_nonzero_curvature evaluates the single- and double-curvature extensions on this field and obtains $\rho,\varepsilon_+$ versus $2\rho,\varepsilon_+$, hence distinct operators at every $\rho\neq 0$ and every resolution.
The construction does not claim a physical curved Lichnerowicz operator: $\rho$ is only a minimal curvature proxy. Closing Gap 4 still requires deriving the genuine curvature endomorphism from curved discrete geometry and proving a $C/N^2$ correction bound so that spectral convergence lifts from the flat theorem. Within Recognition Science gravity, the lemma package shows why flat-spectrum certification alone cannot force the curved coupling that would enter continuum limits of discrete graviton modes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.