planeH_transverse
plain-language theorem explainer
For a polarization with vanishing first row, the axis plane-wave tensor field is exactly discrete-transverse: its forward-difference divergence vanishes at every lattice site and component. Spectral-geometry and discrete-gravity workers cite this when packaging TT-mode convergence of the flat-torus Lichnerowicz spectrum. The proof is a short simp-and-ring reduction: transverse constancy leaves only the longitudinal stencil term, which the row hypothesis kills.
Claim. Fix lattice size $N\in\mathbb{N}$, wavenumber $k\in\mathbb{Z}$, and polarization $\varepsilon\in M_3(\mathbb{C})$ with vanishing first row ($\varepsilon_{0j}=0$ for all $j$). Let $H_{N,k,\varepsilon}$ be the corresponding axis plane-wave tensor field on the 3-torus lattice $\mathbb{Z}^3$. Then for every site $x$ and every component $b\in\{0,1,2\}$, the discrete forward-difference divergence vanishes: $(\mathrm{div}_N H_{N,k,\varepsilon})(x)_b=0$.
background
This module sits in the Seven-Gaps campaign, Lane 4 (operator convergence). It builds a Lean bridge from the discrete perturbation spectrum on a lattice to the continuum Lichnerowicz operator, restricted to the flat 3-torus and to the axis stencil sector only: plane waves with wavevector $(k,0,0)$ acted on by the componentwise axis Laplacian. Lattice sites are Site3 $\simeq \mathbb{Z}\times\mathbb{Z}\times\mathbb{Z}$ with $N$-periodicity along each axis; spacing is $h=1/N$.
An axis plane wave $H_{N,k,\varepsilon}$ is a $3\times 3$ complex matrix field whose spatial dependence is the 1D Fourier mode along the first coordinate and is constant in the transverse coordinates. The discrete divergence discDiv is the forward-difference stencil summed over the three lattice directions. Spatial dimension $D=3$ is the RS-forced value (T8).
The module is explicit that axis stencils are blind to the known anisotropy of the continuum Freudenthal moment tensor, so these identities are not isotropic flat-space recovery of the full Lichnerowicz spectrum.
proof idea
Term-mode proof by simplification then ring. Unfold the discrete divergence and expand the three-term sum over lattice directions. Substitute the pointwise formula for the axis plane wave and the coordinate-shift lemmas for the three unit steps. Because the mode is constant in $y$ and $z$, the transverse difference terms cancel or drop; only the longitudinal ($a=0$) contribution can survive. The hypothesis that the first row of $\varepsilon$ vanishes sets that remaining term to zero. ring closes the resulting algebraic identity.
why it matters
This is the discrete transversality half of the TT package on the flat 3-torus. The parent theorem discrete_tt_spectrum_converges_to_flat_lichnerowicz quotes it as clause (1): for every resolution $N$, every wavenumber, and every polarization with vanishing first row (in particular the plus and cross polarizations), the axis plane wave is exactly discrete-transverse. Clause (2) of that parent is the matching eigenvector identity for the 3D discrete Laplacian.
In the Recognition framework this is operator-convergence scaffolding for gravity on the forced $D=3$ background, not a continuum GR derivation. It closes the discrete side of the TT gauge condition before the eigenvalue limit is taken. The axis-sector mandate remains in force: direction-resolved isotropic recovery is deferred to the separate C10/P-iso probe.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.