epsCross_col0
plain-language theorem explainer
On the axis-sector discrete TT setup, the cross polarization vanishes in every entry of its 0-column: ε^×(i,0)=0 for all spatial indices i. Anyone assembling the two standard TT polarizations for an axis plane wave will cite this. The proof is a three-line fin_cases discharge against the definition of epsCross.
Claim. For every spatial index $i$, the cross-polarization tensor satisfies $\varepsilon^\times_{i0}=0$.
background
The module builds the discrete Lichnerowicz operator on the flat 3-torus and connects its lattice TT spectrum to the continuum operator, restricted to the AXIS stencil sector (plane waves $k=(k,0,0)$ with the componentwise axis Laplacian). Lattice fields are $N$-periodic maps $\mathbb{Z}\to\mathbb{C}$, not functions on $\mathrm{ZMod},N$.
In linearized gravity the transverse-traceless gauge admits a two-dimensional polarization space. For an axis-propagating wave the two standard basis tensors (plus and cross) live in the transverse plane, so any component with a longitudinal index must vanish. Here epsCross is that cross basis; the companion column-zero identity is the discrete bookkeeping of that support restriction. Spatial dimension is the RS-forced $D=3$ (T8).
proof idea
Introduce the spatial index $i$. Because the index type is finite (the three spatial directions), fin_cases i splits into three goals. Each goal reduces by simp against the definition of epsCross, which hard-codes a zero in column 0. No external lemmas are required beyond definitional unfolding.
why it matters
Seven-Gaps Lane 4 (operator convergence) needs an honest discrete TT polarization basis before eigenvalue and symbol statements can be stated. This lemma pins the longitudinal support of the cross mode on the axis sector, so later linear-independence and span claims for the 2D TT space can treat column 0 as identically zero rather than as a side condition.
It sits inside the axis-only scope mandated by panel C14: axis stencils are blind to Freudenthal anisotropy, so this is bookkeeping for axis waves, not isotropic flat-space recovery of the full Lichnerowicz spectrum. No downstream uses are wired yet in the graph; the immediate consumer is the neighboring independence/span theorem for the two standard polarizations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.