axisTTCross
plain-language theorem explainer
Defines the unnormalized cross TT polarization on Fin 4: the symmetric matrix with H_{23}=H_{32}=1 and zeros elsewhere. Gravity analysts cite it as one of the two explicit axis polarizations for the 4D edge TT decomposition. The body is a pure matrix pattern match; no proof.
Claim. Let $H^{\times}\in M_4(\mathbb{R})$ be the symmetric matrix with $H^{\times}_{23}=H^{\times}_{32}=1$ and all other entries zero. This is the unnormalized cross polarization relative to the axis wave covector.
background
This module is the algebraic layer of the QG campaign item edge_tt_decomposition: linear-algebra transverse-traceless decomposition of symmetric real $4\times 4$ matrices against 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.
Mat4 is just $M_4(\mathbb{R})$. A matrix is TT when it is symmetric, Euclidean-traceless, and transverse to the chosen wave covector. The cross mode is the off-diagonal partner of the plus mode on the axis wave vector, with integer entries left unnormalized so later independence and nonzeroness proofs stay elementary.
An equivalent definition already appears upstream in MetricEdgeImage4D as the same symmetric off-diagonal witness $H_{23}=H_{32}=1$.
proof idea
Definition only: pattern-match on $(i,j)\in\mathrm{Fin},4\times\mathrm{Fin},4$, returning $1$ at $(2,3)$ and $(3,2)$ and $0$ elsewhere. No tactics or lemmas.
why it matters
Supplies one of the two explicit independent TT polarizations on the axis wave vector that the module uses to witness "two polarizations in 4D." Immediate parents prove it is TT (axisTTCross_isTT), nonzero (axisTTCross_ne_zero), and linearly independent of the plus mode (axisTT_independent).
Downstream, GeometricFoldVsDictionary4D reuses it as a banked witness: TT against symbolDir, dictionary/moment comparisons, and the honest convergence reading that residual fold equals dictionary at banked witnesses without claiming the hinge moment. It does not close Regge EDGE decomposition, $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$, or gap_action_recovery; those remain outside this algebraic kernel.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.