ttProject_transverse
plain-language theorem explainer
The TT projection of a real 4×4 matrix against a nonzero Euclidean wave covector is transverse: every row contracts to zero with that covector. Gravity analysts cite it when assembling the algebraic TT projector on Fin 4. The proof rewrites the load of the projection via gauge correction and the transverse projector, then cancels both summands.
Claim. Let $m\in\mathbb{R}^4$ satisfy $\sum_k m_k^2\neq 0$, and let $H$ be any real $4\times 4$ matrix. Then the transverse-traceless projection of $H$ against $m$ is transverse: for every row index $i$, $\sum_j (\mathrm{ttProject}\,m\,H)_{ij}\,m_j=0$.
background
This module is the algebraic layer of the QG campaign lane 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 lifts the 3D conventions (Euclidean trace, Euclidean transversality, symmetry) without a Frobenius pin; Minkowski specialization is deferred.
Transversality means the matrix-vector load vanishes: $\mathrm{IsTransverse},m,H$ asserts $\sum_j H_{ij}m_j=0$ for all $i$. The load map packages that contraction as a covector. Gauge correction subtracts the pure-gauge part built from $m$ and $H$, and is already known to be transverse whenever $|m|^2_{\mathrm{Euc}}\neq 0$.
The TT projector is assembled from that gauge-corrected matrix by a further subtraction involving the transverse projector; the present lemma isolates the transversality conjunct of the full algebraic TT predicate.
proof idea
Fix a row index $i$ and restate the goal as vanishing load of the TT projection. Invoke gaugeCorrected_transverse to get that the gauge-corrected matrix already has zero load against $m$. Invoke the companion fact that the transverse projector itself has zero load against $m$. Unfold the definition of the TT projection and apply linearity of load under subtraction and scalar multiplication; both summands cancel, so the load is zero.
why it matters
This is one of the three conjuncts packaged by ttProject_isTT, which asserts that the TT projection of a symmetric matrix is fully algebraic TT (symmetric, Euclidean-traceless, and transverse). The Lorentzian sibling module reuses the same transversality fact (via the Euclidean load identity) inside ttProject_isLorentzTT and its own transverse lemma.
In the Recognition gravity stack this is the kernel-checked algebraic step toward edge TT decomposition on 4D, not yet a continuum or Regge-lattice statement. Module tier tags explicitly withhold claims about Regge EDGE perturbations, $S_{\mathrm{RS}}$ convergence to Einstein-Hilbert in 4D, and gap-action recovery. It sits upstream of those campaign closers as pure linear algebra on $\mathrm{Mat}_4(\mathbb{R})$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.