axisTTPlus_ne_zero
plain-language theorem explainer
The unnormalized plus polarization matrix diag(0,0,1,−1) on Fin 4 is not the zero matrix. Anyone assembling an independent TT pair for the 4D edge transverse-traceless decomposition cites this nondegeneracy. The proof is a one-step contradiction: assume equality to zero, project to the (2,2) entry, and simplify to 1 = 0.
Claim. The unnormalized plus polarization matrix $\mathrm{diag}(0,0,1,-1)$ in $\mathrm{Mat}_4(\mathbb{R})$ is not the zero matrix.
background
This module is the algebraic layer of the QG campaign item edge_tt_decomposition: linear-algebra transverse-traceless structure for symmetric real $4\times 4$ matrices against a nonzero Euclidean wave covector on $\mathrm{Fin},4$. Conventions lift the 3D closer (Euclidean trace, Euclidean transversality, symmetry) without a Frobenius pin; Minkowski/null specialization is deferred.
The plus polarization is the fixed matrix with a single $+1$ at index $(2,2)$ and $-1$ at $(3,3)$, all other entries zero (unnormalized integer entries on the axis wave vector). Nonzeroness is the first sanity check before claiming it as one leg of an independent TT pair.
proof idea
Assume the matrix equals the zero matrix. Apply congruence of the evaluation map $M\mapsto M_{2,2}$ to both sides, then unfold the definition of the plus polarization. The left side becomes $1$ and the right side $0$, contradiction. No external lemmas beyond definitional simplification.
why it matters
In the Recognition Science gravity lane, the 4D edge TT decomposition needs two concrete independent polarizations on the axis wave vector. This lemma certifies that the plus leg is a genuine nonzero matrix, so later TT and independence statements are not vacuous. The module doc places it inside Wave 4 / W4-1 algebraic kernel work: it does not yet decompose Regge EDGE perturbations, prove continuum EH recovery, or flip gap-action recovery. No downstream consumers are wired yet; it is local infrastructure for the TT pair on $\mathrm{Fin},4$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.