epsPlus_isSymm
plain-language theorem explainer
The plus gravitational-wave polarization matrix diag(0, 1, −1) on ℂ³ˣ³ is symmetric. Anyone assembling discrete Lichnerowicz or TT-gauge mode expansions on the flat 3-torus cites this. The proof is pure finite case analysis: extend equality of matrix entries and discharge all Fin 3 pairs by simplification against the definition.
Claim. The plus polarization matrix $\varepsilon_+ = \mathrm{diag}(0,1,-1) \in M_3(\mathbb{C})$ is symmetric: $(\varepsilon_+)_{ij} = (\varepsilon_+)_{ji}$ for all $i,j \in \{0,1,2\}$.
background
This module builds the discrete Lichnerowicz operator on the flat 3-torus as part of the Seven-Gaps campaign (Lane 4: operator convergence). Lattice functions are N-periodic maps ℤ → ℂ with spacing h = 1/N; 3D sites are ℤ³ with axial periodicity. Convergence results here are restricted to the axis stencil sector (plane waves k = (k,0,0) under the componentwise axis Laplacian), not full isotropic recovery of the continuum spectrum.
The plus polarization is the constant matrix ε₊ = diag(0, 1, −1) in M₃(ℂ). Together with the cross polarization (the symmetric off-diagonal E₂₃ + E₃₂), it supplies the two TT helicity templates used when expanding discrete metric perturbations. Symmetry of these templates is the elementary algebraic prerequisite before any discrete inner product or self-adjointness argument for the Lichnerowicz stencil.
proof idea
Term-mode proof by matrix extensionality: it suffices that every entry (i,j) equals (j,i). Both indices run over Fin 3, so fin_cases enumerates the nine pairs; each goal reduces by simp against the literal definition of ε₊ (only the (1,1) and (2,2) diagonal entries are nonzero, and they already match under swap). No external lemmas are required.
why it matters
In the discrete Lichnerowicz development, polarization matrices must be symmetric so that the discrete operator stays formally self-adjoint on TT modes and so that the Fourier-mode eigenvalue identities remain consistent with continuum GW helicities. This lemma closes that algebraic obligation for the plus channel on the flat 3-torus background.
It sits inside the axis-sector program flagged by the module doc: results here must not be read as isotropic flat-space recovery of the full Lichnerowicz spectrum (Freudenthal stencil anisotropy is deferred to the C10 probe). No downstream theorems currently depend on it in the graph, so it is infrastructure for forthcoming discrete TT-mode and spectrum-convergence statements rather than a cited parent itself. Framework landmarks touched only indirectly: D = 3 (T8) fixes the 3×3 matrix size.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.