IsTransverse
plain-language theorem explainer
A real 4×4 matrix is transverse to a Euclidean wave covector m when the matrix–vector product vanishes: Hm = 0. This is the third algebraic conjunct of the 4D transverse-traceless condition, lifted from the 3D IsTTPolarization conventions. Gravity and continuum-preflight lemmas cite it to certify gauge-corrected and projected loads. The body is a one-line Prop abbreviation, not a proved statement.
Claim. A matrix $H \in M_4(\mathbb{R})$ is transverse to a covector $m \in \mathbb{R}^4$ when $\sum_{j=0}^{3} H_{ij} m_j = 0$ for every row index $i \in \{0,1,2,3\}$, i.e. $Hm = 0$.
background
The module is the algebraic layer of the QG campaign ledger name edge_tt_decomposition: linear-algebra TT decomposition of symmetric real $4\times 4$ matrices against a nonzero Euclidean wave covector on $\mathrm{Fin},4$. It inherits three Euclidean conjuncts from the 3D closer chain (symmetry, Euclidean trace zero, transversality) and lifts them without a Frobenius pin; Minkowski/null specialization is deferred.
Here $H$ is a plain matrix (Mat4 $= M_4(\mathbb{R})$), not the Recognition cost reparametrization. Transversality means the load $Hm$ vanishes componentwise: each row of $H$ is orthogonal to $m$. Together with symmetry and Euclidean tracelessness this defines algebraic TT.
proof idea
Definitional Prop, not a theorem. The body is the universal quantification $\forall i,;\sum_j H_{ij}m_j=0$, i.e. the matrix–vector product $Hm=0$. Downstream proofs typically intro i and rewrite the sum as the local load helper, then cancel gauge pieces.
why it matters
Third conjunct inside IsTT (symmetric $\wedge$ Euclidean-traceless $\wedge$ transverse), so every algebraic TT certificate in this file routes through it. Downstream uses include gaugeCorrected_transverse and ttProject_transverse (projection restores transversality when $m\cdot m\neq 0$), decoy lemmas showing longitudinal/gauge junk fails transversality, and the continuum preflight edge_tt_decomposition / smul_preserves_transverse. It is the 4D lift of the Euclidean transversality half of 3D IsTTPolarization, and is required before any claim about two independent TT polarizations on an axis wave vector. It does not itself close Regge EDGE perturbations or $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.