discLap3_constantPlusField_zero
plain-language theorem explainer
The componentwise flat lattice Laplacian kills the constant plus-polarized tensor field at every lattice resolution N. Gravity Gap-4 arguments cite this to show both curvature-coupled operator families share the same flat zero mode. The proof is a short pointwise algebraic reduction: expand the three-neighbor stencil and cancel by ring.
Claim. For every lattice size $N\in\mathbb{N}$, if $u$ is the constant plus-polarized lattice tensor field ($u(x)=\varepsilon_+$ at every site), then the componentwise discrete Laplacian satisfies $\Delta_3^{(N)} u = 0$.
background
Gap 4 in the gravity stack records that the certified spectrum theorem for the discrete Lichnerowicz operator only treats axis modes of the componentwise flat lattice Laplacian. Its continuum value is definitional from the flat reduction $\Delta_L=-\Delta$, with no Riemann endomorphism, so it cannot fix a curved-background coupling.
This module exhibits that underdetermination explicitly. On the lattice tensor-field type it builds two zeroth-order curvature-coupled families that both specialize to $-\mathrm{discLap}_3$ at zero curvature, yet disagree on a concrete nonzero TT polarization whenever curvature is nonzero.
The constant plus field is the constant map sending every lattice site to the fixed plus polarization $\varepsilon_+$. The operator $\mathrm{discLap}_3,N$ is the three-direction discrete Laplacian from DiscreteLichnerowicz. Annihilating this constant field is the elementary zero-mode fact needed before comparing flat specializations of the two curved extensions.
proof idea
Term-mode proof by pointwise identity. Apply function extensionality on lattice sites, then matrix extensionality on tensor indices. Unfold discLap3 and constantPlusField; the field is site-independent, so neighbor differences vanish. Rewrite the three-term sum over Fin 3 via Fin.sum_univ_three and finish by ring. No external lemmas beyond simp lemmas for zero and matrix application.
why it matters
This is a local algebraic lemma inside the Gap 4 blocker module: flat spectrum does not determine curvature coupling. It certifies that the distinguishing constant plus field is a genuine flat zero mode of $\mathrm{discLap}_3$, so both curvature-coupled families can share the same complete flat specialization while still splitting at nonzero curvature proxy $\rho$.
Downstream siblings (flat specialization agreement, distinctness at nonzero curvature, curved eigenvalue branches) rely on having a concrete field that the flat operator kills. The module does not claim a physical curved Lichnerowicz operator; $\rho$ is only a minimal proxy. Closing Gap 4 still requires deriving the genuine curvature endomorphism from curved discrete geometry and a $C/N^2$ correction bound feeding eigenvalue_limit_of_uniform_bound.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.