epsPlus_col0
plain-language theorem explainer
The plus-polarization matrix has a vanishing first column: every entry in column index 0 is zero. Anyone assembling TT projectors or checking that the plus mode is orthogonal to a propagation axis along the first coordinate would cite this. The proof is a three-line case split on the row index with simplification against the matrix literal.
Claim. For every row index $i \in \{0,1,2\}$, the matrix entry $(\varepsilon^+)_{i0}$ equals $0$, where $\varepsilon^+ = \mathrm{diag}(0,1,-1)$ is the plus-polarization matrix on $\mathbb{C}^{3\times 3}$.
background
The ambient module constructs the discrete Lichnerowicz operator on the flat 3-torus and proves axis-sector spectrum convergence (Seven-Gaps Lane 4). Lattice fields are $N$-periodic maps $\mathbb{Z}\to\mathbb{C}$ with spacing $h=1/N$; 3D sites are $\mathbb{Z}^3$ with axis periodicity. All convergence statements are restricted to plane waves $k=(k,0,0)$ under the componentwise axis-stencil Laplacian, and must not be read as isotropic recovery of the full continuum spectrum.
The plus polarization is the constant matrix $\varepsilon^+=\mathrm{diag}(0,1,-1)$. In the standard TT gauge with propagation along the first axis, this is the $+$ gravitational-wave polarization: it is traceless, symmetric, and has vanishing first row and column, so it is transverse to that axis. The companion cross polarization is $E_{23}+E_{32}$.
proof idea
Introduce the row index $i:\mathrm{Fin},3$. Case-split on the three concrete values of $i$, then simplify each goal against the matrix literal definition of the plus polarization. Every entry in column 0 is the constant $0$ in that literal, so each case closes immediately.
why it matters
Column vanishing is the elementary algebraic content of transversality for the $+$ mode when the wave vector lies along the first coordinate. In the discrete Lichnerowicz development it is bookkeeping that keeps polarization tensors aligned with the axis-sector stencil and the Fourier-mode eigenvalue identities already proved in-module (discLap_fourierMode and companions).
No downstream consumer is wired yet in the dependency graph. The result sits inside the honest THEOREM tier of the module (axiom-clean matrix facts supporting operator convergence) and does not touch continuum isotropy, the Freudenthal anisotropy probe, or the open C10 direction-resolved symbol question. Framework landmarks T0–T8 and the RCL are not directly implicated; this is pure discrete-gravity linear algebra on the flat torus background.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.