epsPlus
plain-language theorem explainer
The plus polarization is the fixed complex 3×3 matrix diag(0,1,−1). It is the standard TT + mode used throughout the discrete Lichnerowicz development on the flat 3-torus and as a constant witness field that separates curvature extensions. The declaration is a pure matrix literal; no proof content.
Claim. Define the plus polarization $\varepsilon_+ \in M_3(\mathbb{C})$ by $\varepsilon_+ = \mathrm{diag}(0,1,-1)$, i.e. the matrix with $1$ in the $(2,2)$ entry, $-1$ in the $(3,3)$ entry, and zeros elsewhere.
background
The module sits in the Seven-Gaps campaign, Lane 4 (operator convergence). It builds a Lean link between the discrete perturbation spectrum on a lattice and the continuum Lichnerowicz operator, restricted to the flat 3-torus background and the axis stencil sector only (plane waves $k=(k,0,0)$ under the componentwise axis Laplacian). Axis stencils are blind to the known Freudenthal anisotropy, so results here are not isotropic full-spectrum recovery.
Lattice fields are $N$-periodic maps $\mathbb{Z}\to\mathbb{C}$ (spacing $h=1/N$), not functions on $\mathrm{ZMod},N$. Tensor polarizations live in $M_3(\mathbb{C})$ and label the two TT gravitational-wave modes. The plus mode is the diagonal traceless pattern $\mathrm{diag}(0,1,-1)$; the sibling cross mode is the off-diagonal $E_{23}+E_{32}$ pattern. Both are used as constant or Fourier-modulated tensor fields on the lattice.
proof idea
Definitional matrix literal. The body is the Mathlib !![...] constructor writing the three rows $[0,0,0]$, $[0,1,0]$, $[0,0,-1]$ over $\mathbb{C}$. No tactics, lemmas, or computation.
why it matters
Supplies the canonical + polarization for the discrete Lichnerowicz stack. Immediate consumers prove it is symmetric, traceless, and has vanishing first row and column (the TT gauge conditions on a fixed background). Those facts feed polarizations_linearIndependent and the flat eigenvalue identity lichnerowiczFlatEigenvalue.
Downstream, constantPlusField is the constant lattice tensor field with value $\varepsilon_+$ at every site. That field is the witness in extensions_distinct_at_nonzero_curvature: the flat Laplacian annihilates it, while the two curvature-coefficient extensions act by $\rho$ and $2\rho$, so the operators differ at every nonzero curvature and every resolution. The definition is therefore the concrete algebraic seed for both the flat TT spectrum work and the curved-operator underdetermination argument in Lane 4.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.