epsPlus_row0
plain-language theorem explainer
The plus-polarization matrix has a vanishing first row: every entry in row 0 is zero. Gravity and discrete-spectrum work on the flat 3-torus cites this when assembling TT polarizations for the discrete Lichnerowicz operator. The proof is a three-way case split on Fin 3 followed by simplification against the matrix literal.
Claim. Let $\varepsilon^+$ be the plus polarization matrix $\mathrm{diag}(0,1,-1)$ on $\mathbb{C}^{3\times 3}$. Then for every column index $j\in\{0,1,2\}$, the entry $(\varepsilon^+)_{0j}$ equals $0$.
background
The module builds the discrete Lichnerowicz operator on the flat 3-torus and connects 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 axis periodicity. Convergence results here are restricted to the axis stencil sector (plane waves $k=(k,0,0)$ under the componentwise axis Laplacian).
The plus polarization is the constant matrix $\varepsilon^+=\mathrm{diag}(0,1,-1)$ in $\mathrm{Mat}{3\times 3}(\mathbb{C})$, the standard TT $+$ mode for gravitational waves in a fixed Cartesian frame. Its first row (and first column) vanishes by construction, encoding that the polarization is transverse to the chosen propagation axis $e_0$. A sibling cross polarization $E{23}+E_{32}$ completes the usual TT pair.
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 epsPlus, whose matrix literal has first row $(0,0,0)$. No external lemmas are required.
why it matters
In the discrete Lichnerowicz setup, TT polarizations seed the discrete metric perturbations whose eigenvalues are compared to the continuum Lichnerowicz spectrum on $T^3$. Vanishing of row 0 is the elementary algebraic fact that $\varepsilon^+$ is transverse to the axis direction used by the axis-sector stencil. The module is explicit that axis-sector results must not be read as isotropic flat-space recovery of the full Lichnerowicz spectrum (Freudenthal energy anisotropy; C10 probe). No downstream consumers are wired yet; the lemma is local scaffolding for polarization identities inside this file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.