axisTTCross_ne_zero
plain-language theorem explainer
The unnormalized cross TT polarization on the axis wave vector is a nonzero 4×4 matrix: its (2,3) and (3,2) entries equal 1. Anyone building an independent TT pair for the 4D edge decomposition cites this nondegeneracy. The proof is a one-line entry extraction: equality to zero would force the (2,3) entry to vanish, contradicting the definition.
Claim. The cross polarization matrix $H$ with $H_{23}=H_{32}=1$ and all other entries zero is not the zero matrix in $\mathrm{Mat}_4(\mathbb{R})$.
background
This module is the algebraic layer of the QG campaign item edge_tt_decomposition: the linear-algebra transverse-traceless (TT) decomposition of symmetric real $4\times 4$ matrices relative to a nonzero Euclidean wave covector on $\mathrm{Fin},4$. Conventions lift the 3D closer chain (Euclidean trace, Euclidean transversality, symmetry) without a Frobenius pin; Minkowski/null specialization is deferred.
The cross mode is the explicit matrix with sole nonzero entries $H_{23}=H_{32}=1$ (unnormalized integer data). Together with a plus-type axis mode it is meant to supply an independent TT pair witnessing two polarizations in 4D. Nonzeroness is the first sanity check before symmetry, tracelessness, and transversality are verified for that pair.
proof idea
Assume for contradiction that the cross matrix equals the zero matrix. Apply congruence of the $(2,3)$ entry map on $\mathrm{Mat}_4$. Unfolding the definition of the cross matrix yields $1=0$, which is absurd. The argument is pure entrywise evaluation; no TT or metric lemmas are required.
why it matters
In the Recognition Science gravity stack this sits inside Wave 4 / lane W4-1, the smallest kernel-checked increment toward ledger closing name edge_tt_decomposition. It does not yet decompose Regge EDGE perturbations, prove continuum EH recovery, or flip gap_action_recovery; those are explicitly out of scope for the algebraic layer.
Nondegeneracy of the cross witness is a prerequisite for any later claim that the axis plus/cross pair spans a two-dimensional TT space on the chosen wave vector. No downstream theorems currently depend on it in the graph, so it is infrastructure for the independent-pair construction rather than a cited parent lemma. Framework landmarks T0–T8 and the RCL are not directly invoked here; the link is only through the broader 4D gravity campaign.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.