planeH_shift_yz
plain-language theorem explainer
Axis plane waves on the 3D lattice are invariant under arbitrary shifts in the transverse (y,z) directions, hence periodic along those axes. Cite this when setting up the axis-sector discrete Lichnerowicz spectrum on the flat 3-torus. The proof unfolds the plane-wave definition and applies add-zero on the longitudinal coordinate.
Claim. For lattice period $N\in\mathbb{N}$, wave number $k\in\mathbb{Z}$, polarization $\varepsilon\in M_3(\mathbb{C})$, site $x\in\mathbb{Z}^3$, and $s,t\in\mathbb{Z}$, the axis plane wave satisfies $H_N^{k,\varepsilon}\bigl(x+(0,s,t)\bigr)=H_N^{k,\varepsilon}(x)$.
background
This module builds the discrete Lichnerowicz operator on the flat 3-torus and proves axis-sector spectrum convergence (Seven-Gaps Lane 4). Lattice sites are Site3 := $\mathbb{Z}\times\mathbb{Z}\times\mathbb{Z}$, read as the periodic flat 3-torus. Lattice tensor fields assign a $3\times 3$ complex matrix at each site.
Axis plane waves factor as a 1D Fourier mode $\mathrm{e}^{2\pi i k j/N}$ along the longitudinal coordinate, tensored with a constant polarization matrix $\varepsilon$. The mode is independent of the transverse coordinates. Representation is via $N$-periodic maps $\mathbb{Z}\to\mathbb{C}$ (spacing $h=1/N$), not ZMod N, so stencil identities hold pointwise and torus periodicity is grounded by mode periodicity lemmas.
Scope is strictly the axis stencil sector: plane waves with wavevector $(k,0,0)$ under the componentwise axis Laplacian. Axis stencils are blind to Freudenthal anisotropy, so these results are not isotropic flat-space recovery of the full Lichnerowicz spectrum.
proof idea
One-step reduction. Unfold the axis plane wave at the shifted site: the definition depends only on the first coordinate of the site, so $H$ at $x+(0,s,t)$ is $\mathrm{fourierMode},N,k,(x_1+0),\bullet,\varepsilon$. Rewrite with add_zero to drop the $0$, matching the unshifted value $\mathrm{fourierMode},N,k,x_1,\bullet,\varepsilon$. Transverse integers $s,t$ never enter the scalar mode.
why it matters
Together with axis periodicity, this lemma grounds the flat 3-torus interpretation of axis plane waves in the discrete Lichnerowicz file: modes are constant (hence periodic) in $y$ and $z$. The module lists it among the representation facts that make stencil and eigenvalue identities torus-ready without ZMod wraparound.
It feeds the axis-sector pipeline toward discrete-to-continuum Lichnerowicz convergence on $T^3$ (Lane 4 operator-convergence gap). The next documented step in the same file is discrete transversality: for polarizations with vanishing first row, the forward-difference divergence of the axis plane wave vanishes identically, using constancy in $y,z$ plus $\varepsilon_{0b}=0$.
No downstream uses are wired yet in the graph. Framework-wise this is lattice analysis infrastructure for gravity, not a T0–T8 forcing step; it supports the discrete side of the continuum limit comparison under the axis-sector mandate (C14).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.