axisTTCross_isTT
plain-language theorem explainer
The unnormalized cross polarization matrix with only H_{23}=H_{32}=1 is algebraically transverse-traceless against the axis wave covector (1,0,0,0). Gravity and continuum-limit authors cite it when fixing an explicit independent TT pair on Fin 4. The proof is a three-conjunct refine that discharges symmetry, Euclidean tracelessness, and transversality by exhaustive Fin 4 case analysis.
Claim. Let $H$ be the $4\times 4$ real matrix with $H_{23}=H_{32}=1$ and all other entries zero, and let $m=(1,0,0,0)$. Then $H$ is symmetric, has vanishing Euclidean trace $\sum_i H_{ii}=0$, and is transverse to $m$ (i.e., $\sum_j H_{ij}m_j=0$ for all $i$). Equivalently, $H$ is algebraically TT with respect to $m$.
background
This module is the algebraic layer of the QG campaign lane edge_tt_decomposition: linear-algebra TT structure for symmetric $4\times 4$ real matrices against a nonzero Euclidean wave covector on Fin 4. It lifts the 3D conventions (Euclidean trace, Euclidean transversality, symmetry) without a Frobenius pin; Minkowski/null specialization is deferred.
Algebraic TT means the conjunction of three props: symmetry of $H$, vanishing Euclidean trace $\sum_{i=0}^{3} H_{ii}=0$, and transversality $\sum_j H_{ij}m_j=0$ for every row. The axis wave is the fixed covector $m=(1,0,0,0)$. The cross polarization is the unnormalized integer matrix with sole nonzero entries $H_{23}=H_{32}=1$, the second of an explicit independent TT pair on that axis.
The parent decomposition theorem states every symmetric matrix against nonzero $m$ splits as TT plus gauge plus transverse-trace residual; the present result supplies one concrete TT witness used downstream when normalizing that pair.
proof idea
Term-mode refine of the three conjuncts of algebraic TT.
Symmetry: introduce indices $i,j$ and run fin_cases on both; every entry equality is definitional (rfl).
Tracelessness: unfold Euclidean trace and the cross matrix, then simp with the four-term Fin sum; the diagonal is identically zero.
Transversality: for each row index, fin_cases and simp against the definitions of the cross matrix and axis wave together with the four-term sum; only the $m_0=1$ component can contribute, and the first row/column of the cross matrix vanishes.
No external lemmas beyond the in-module defs and Fin enumeration.
why it matters
Supplies a kernel-checked explicit TT witness for the algebraic edge_tt_decomposition layer (Wave 4 / W4-1). Downstream, axisTTCrossNormalized_isTT in the Regge 4D continuum preflight reuses the symmetry conjunct via axisTTCross_isTT.1 when scaling the same matrix, so the normalized cross polarization inherits TT status.
In the broader Recognition gravity stack this is scaffolding for continuum recovery of Einstein-Hilbert from the RS action on 4D lattices: two independent polarizations on a fixed axis wave are the algebraic stand-in for the two graviton helicities before Lorentzian specialization. It does not itself close S_RS_converges_EH_4d or flip gap_action_recovery; those remain separate campaign targets. The result sits strictly inside the Euclidean algebraic tier tagged THEOREM in the module doc.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.