polarizations_linearIndependent
plain-language theorem explainer
The plus and cross TT polarization matrices are linearly independent over ℂ, so they give a 2D basis for axis-wave polarizations on the flat 3-torus. Cite this when assembling discrete Lichnerowicz / TT mode spaces in the Seven-Gaps operator-convergence lane. The proof is a direct Fin-2 independence check by reading two matrix entries.
Claim. The standard plus and cross polarization matrices $\varepsilon_+,\varepsilon_\times\in M_3(\mathbb{C})$ (with $\varepsilon_\times=E_{23}+E_{32}$) are linearly independent over $\mathbb{C}$.
background
This module builds a discrete-to-continuum link for the Lichnerowicz operator on the flat 3-torus (Seven-Gaps Lane 4: operator convergence). Lattice fields are $N$-periodic maps $\mathbb{Z}\to\mathbb{C}$ with spacing $h=1/N$; the axis-sector stencil Laplacian acts on plane waves $k=(k,0,0)$ only. Axis results must not be read as isotropic flat-space recovery of the full spectrum (Freudenthal energy is anisotropic).
For a wave along the first axis, the two standard transverse-traceless polarizations are the symmetric matrices $\varepsilon_+$ (plus) and $\varepsilon_\times$ (cross). The cross polarization is defined entrywise as $E_{23}+E_{32}$, i.e. the matrix with $1$s in the $(1,2)$ and $(2,1)$ slots (0-indexed Fin 3) and zeros elsewhere. Linear independence of these two matrices is the elementary algebraic fact that they span a genuine 2D TT polarization space before any spectral analysis.
proof idea
Rewrite via Mathlib's linearIndependent_fin2, which reduces independence of a length-2 family to: the second vector is nonzero, and no scalar multiple of the second equals the first.
First branch: if $\varepsilon_\times=0$, compare the $(1,2)$ entry. That entry of $\varepsilon_\times$ is $1$ by definition, while the zero matrix has $0$ there, so $1=0$, contradicting one_ne_zero.
Second branch: if $a\cdot\varepsilon_\times=\varepsilon_+$, compare the $(1,1)$ entry. The left side is $a\cdot 0=0$ (mul_zero); the right side is $1$ by the plus matrix. Hence $0=1$, contradicting zero_ne_one.
No spectral or continuum input is used; only matrix entry evaluation and the two nontriviality lemmas.
why it matters
In the discrete Lichnerowicz development, TT gravitational-wave modes on the axis sector are built from Fourier profiles tensored with a 2D polarization space. This theorem certifies that the classical plus/cross pair is free over $\mathbb{C}$, so that space is genuinely two-dimensional rather than collapsed.
It sits in the MODEL-layer polarization setup that precedes the flat Lichnerowicz connection and the eigenvalue-convergence statements (discLap_fourierMode, discreteEigenvalue_tendsto, and siblings). The module doc tags those convergence results as THEOREM-tier along the axis stencil only.
No downstream consumers are wired yet (used_by empty). The result does not touch the forcing chain (T0–T8), RCL, or $\phi$-ladder mass formulae; it is pure linear algebra supporting the gravity operator-convergence gap. The open direction-resolved symbol question (C10 / isotropic recovery) remains separate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.