epsCross
plain-language theorem explainer
The standard cross TT polarization on a 3-torus: the symmetric traceless matrix with 1's in the (2,3) and (3,2) slots and zeros elsewhere. Gravity and discrete-spectrum workers cite it as one of the two basis tensors for axis-directed plane-wave perturbations. It is a literal matrix literal, not a derived construction.
Claim. Define the cross polarization matrix $\varepsilon^\times \in M_3(\mathbb{C})$ by $\varepsilon^\times = E_{23}+E_{32}$, i.e. the matrix with $1$ in positions $(2,3)$ and $(3,2)$ and $0$ elsewhere (1-based spatial indices $1,2,3$).
background
The module treats the discrete Lichnerowicz operator on the flat 3-torus, as part of the Seven-Gaps "operator convergence" lane. Lattice fields are $N$-periodic maps $\mathbb{Z}\to\mathbb{C}$ (spacing $h=1/N$), and 3D sites are $\mathbb{Z}^3$ with axial periodicity. Convergence statements here are restricted to the axis stencil sector: plane waves $k=(k,0,0)$ under the componentwise axis Laplacian.
In continuum GR, transverse-traceless (TT) metric perturbations on a Ricci-flat background are the physical GW degrees of freedom. For a wave along the first axis, the two standard linear polarizations are plus and cross. The cross mode is the off-diagonal $yz$ strain: the matrix unit sum $E_{23}+E_{32}$.
Sibling objects include the discrete Laplacian, Fourier modes, and the plus polarization matrix. Downstream lemmas check that this matrix is symmetric, traceless, and has vanishing first row and column (transverse to an $x$-directed wave).
proof idea
No proof: a one-line matrix definition via the !![·;·;·] literal. The entries are the constants $0$ and $1$ in $\mathbb{C}$, arranged so that only the $(1,2)$ and $(2,1)$ zero-based slots (spatial $yz$) are nonzero.
why it matters
Supplies one of the two standard TT polarization tensors used throughout the discrete Lichnerowicz development. Downstream, epsCross_isSymm, epsCross_traceless, epsCross_row0, and epsCross_col0 certify the TT algebraic constraints (symmetric, trace-free, transverse to an axis wave). Together with the plus polarization they feed polarizations_linearIndependent, which states they span the 2D TT polarization space for the axis wave.
That basis is what lets the package compare discrete eigenvalues of lattice TT modes to the flat-background continuum model eigenvalue $(2\pi k)^2$ (Lichnerowicz reducing to $-\nabla^2$ when Riemann vanishes). In the broader RS gravity program this is scaffolding for Lane 4 operator convergence on $T^3$, not a claim about curved backgrounds or full isotropic Freudenthal stencils (axis sector only; anisotropy is deferred to the C10 probe).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.