ttProject_transverse
plain-language theorem explainer
For any non-null Minkowski wave covector m and any 4×4 real matrix H, the algebraic TT projection of H against m is Lorentz-transverse: contracting each row with the raised m vanishes. Gravity and GR-linearization workers cite it when assembling the full Lorentz TT certificate. The proof subtracts a residual-trace multiple of the transverse projector from the already-transverse gauge correction and cancels both load terms.
Claim. Let $m\in\mathbb{R}^{4}$ satisfy $m\cdot_{\eta} m\neq 0$ and let $H$ be any real $4\times 4$ matrix. Then the algebraic TT projection $\mathrm{TT}(m,H)$ is Lorentz-transverse: for every index $i$, $-(H^{\mathrm{TT}})_{i0}m_{0}+(H^{\mathrm{TT}})_{i1}m_{1}+(H^{\mathrm{TT}})_{i2}m_{2}+(H^{\mathrm{TT}})_{i3}m_{3}=0$.
background
This module is the Lorentzian algebraic layer of the QG campaign lane edge_tt_decomposition (Wave 4 / W4-1). It specializes the Euclidean TT layer of EdgeTTDecomposition4D to signature $(-+++)$ on Fin 4, including the physically relevant null case, without yet touching Regge edge perturbations or Einstein–Hilbert recovery.
Covectors are lowered by default. Index raising negates the time component. The Minkowski pairing is $m\cdot_{\eta}n=-(m_{0})(n_{0})+\sum_{k=1}^{3}m_{k}n_{k}$. Lorentz transversality contracts the second index of $H$ against the raised wave covector. In the non-null sector $m\cdot_{\eta}m\neq 0$ the projector is $P_{ij}=\eta_{ij}-m_{i}m_{j}/(m\cdot m)$.
The TT projection is built as $\mathrm{TT}(m,H)=\mathrm{gaugeCorrected}(m,H)-(\mathrm{residual,trace})\cdot P(m)$, where gauge correction already kills the longitudinal load. The Euclidean sibling ttProject_transverse and the local gaugeCorrected_transverse supply the same load-cancellation pattern with Euclidean load replaced by Lorentz load.
proof idea
Fix a row index $i$. Rewrite the Lorentz-transversality goal as vanishing of the Lorentz load of $\mathrm{TT}(m,H)$ on $m$. Split the load across the definition $\mathrm{TT}=\mathrm{gaugeCorrected}-c,P$. The gauge-corrected summand has load zero by gaugeCorrected_transverse (after equating load notations). The projector summand has load zero by lorentzLoad_transverseProjector. Linearity of Lorentz load under subtraction and scalar multiplication then finishes by simp.
why it matters
This is one of the three legs of the algebraic Lorentz TT certificate. Downstream, ttProject_isLorentzTT packages symmetry, Minkowski-tracelessness, and this transversality into IsLorentzTT m (ttProject m H). The Euclidean parent ttProject_isTT uses the same pattern.
In the Recognition Science gravity stack the result sits inside the ledger-closing name edge_tt_decomposition: it supplies the linear-algebraic TT projector needed before any continuum or lattice identification with Einstein–Hilbert dynamics. It does not itself flip gap_action_recovery or prove $S_{\mathrm{RS}}\to S_{\mathrm{EH}}$. It is the non-null half of the Lorentzian layer; the null projector (auxiliary $l$ with $m\cdot l\neq 0$) is handled separately in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.