epsCross_row0
plain-language theorem explainer
The cross-polarization matrix has a vanishing first row: every entry in row index 0 is zero. Anyone assembling TT polarization tensors on the flat 3-torus lattice cites this when restricting to the transverse-traceless sector. The proof is a three-way Fin case split followed by simplification against the explicit matrix.
Claim. For every column index $j \in \{0,1,2\}$, the entry $(\varepsilon^\times)_{0j}$ of the cross-polarization matrix equals $0$. Equivalently, the first row of $\varepsilon^\times = E_{23}+E_{32}$ is identically zero.
background
The module develops the discrete Lichnerowicz operator on the flat 3-torus, connecting lattice perturbation spectra to the continuum operator (Seven-Gaps Lane 4, operator convergence). Lattice functions are $N$-periodic maps $\mathbb{Z}\to\mathbb{C}$ with spacing $h=1/N$; 3D sites are $\mathbb{Z}^3$ with axiswise periodicity. All convergence results here are restricted to the axis-stencil sector (plane waves $k=(k,0,0)$ under the componentwise Laplacian), and must not be read as isotropic recovery of the full Lichnerowicz spectrum.
The cross-polarization matrix $\varepsilon^\times$ is the explicit $3\times 3$ complex matrix with sole nonzero entries $(\varepsilon^\times){12}=(\varepsilon^\times){21}=1$, i.e. $E_{23}+E_{32}$ in the standard basis. It is the discrete stand-in for the continuum cross TT polarization. Row 0 corresponds to the first spatial axis; vanishing there is the elementary algebraic content of that matrix definition.
proof idea
Introduce the column index $j:\mathrm{Fin},3$. Case-split on the three values of $j$ via fin_cases, then simplify each goal against the definition of epsCross. Every entry in the first row of the literal matrix !![0,0,0; 0,0,1; 0,1,0] is definitionally zero, so each subgoal closes by simp.
why it matters
In the discrete TT setup for the flat-torus Lichnerowicz spectrum, polarization matrices must be transverse and traceless. Vanishing of the first row of $\varepsilon^\times$ is a basic structural fact used when checking that cross modes sit in the correct algebraic sector before eigenvalue or convergence arguments. The module sits in the Seven-Gaps gravity campaign (Lane 4), building the first Lean bridge from lattice Fourier modes to continuum Lichnerowicz eigenvalues on $T^3$, under the axis-sector caveat. No downstream consumers are wired yet in the graph; the lemma is local scaffolding for polarization bookkeeping rather than a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.