planeH_periodic_axis
plain-language theorem explainer
Axis plane waves on the discrete flat 3-torus are N-periodic along the propagation axis, grounding the torus reading of lattice tensor fields. Anyone working the Seven-Gaps operator-convergence lane (axis sector) cites this when treating plane-wave test fields as living on T^3. The proof is a one-line rewrite through scalar Fourier-mode periodicity.
Claim. For every lattice size $N\in\mathbb{N}$, wavenumber $k\in\mathbb{Z}$, constant polarization $\varepsilon\in M_3(\mathbb{C})$, and site $x\in\mathbb{Z}^3$, the axis plane wave $H_{N,k,\varepsilon}(x)=e^{2\pi i k x_1/N}\,\varepsilon$ satisfies $H_{N,k,\varepsilon}(x+(N,0,0))=H_{N,k,\varepsilon}(x)$.
background
The module builds a Lean bridge from the discrete perturbation spectrum on a lattice to the continuum Lichnerowicz operator, restricted to the flat 3-torus and the axis stencil sector only. Lattice sites are Site3 := ℤ × ℤ × ℤ, read as the flat 3-torus once N-periodicity along each axis is established. Lattice tensor fields assign a 3×3 complex matrix to every site.
The scalar building block is the Fourier mode $j\mapsto\exp(2\pi i k j/N)$ on the N-site discrete circle. The axis plane wave multiplies that 1D mode in the first coordinate by a fixed polarization matrix, so the wavevector is strictly $(k,0,0)$. Representation is as N-periodic maps $ℤ\toℂ$, not as functions on ZMod N, so stencil identities hold pointwise and torus grounding is exactly periodicity of the modes.
Upstream, fourierMode_periodic already records that the scalar mode is N-periodic (trivial when N=0). Axis-sector scope is deliberate: Freudenthal frozen-energy tests show the continuum moment tensor is anisotropic, so axis stencils must not be read as isotropic flat-space recovery of the full Lichnerowicz spectrum.
proof idea
Unfold the definition of the axis plane wave: both sides are the scalar Fourier mode (evaluated at the first coordinate) times the same polarization matrix. After a shift by $(N,0,0)$, only the first coordinate changes, by $+N$. Rewrite that scalar factor with fourierMode_periodic, which supplies $N$-periodicity of $j\mapsto\exp(2\pi i k j/N)$. The matrix factor is unchanged, so equality follows. Term-mode, essentially one rewrite.
why it matters
This is one of the two torus-grounding facts named in the module header (periodicity along the wave axis; the companion is transverse shift invariance). Without it, axis plane waves would be functions on $ℤ^3$ rather than fields on the flat 3-torus, and the discrete-to-continuum Lichnerowicz comparison in Seven-Gaps Lane 4 would lack a compact background.
It sits in the proved tier of the axis-sector campaign: Fourier modes as eigenvectors of the spacing-normalized discrete Laplacian, discrete eigenvalues, and their continuum limit are the neighboring landmarks. Framework-wise it supports the D=3 spatial lattice setting used throughout the gravity gaps work, but only along axis wavevectors $k=(k,0,0)$ under the componentwise axis stencil.
No downstream consumers are wired yet in the graph; the lemma is infrastructure for any later identity that moves plane-wave test fields around the torus or quotients by the lattice period.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.