nullTTProject_transverse_m
plain-language theorem explainer
For a null Minkowski covector m and auxiliary l with nonzero pairing, the null TT projection of any real 4×4 matrix is Lorentz-transverse to m. Gravity analysts in the edge TT campaign cite this when packaging the full algebraic TT property in the null sector. The proof reduces the claim to vanishing Lorentz loads of the null projector and a companion load identity, then simplifies by linearity.
Claim. Let $m,l:\mathbb{R}^4$ satisfy $m\cdot m=0$ and $m\cdot l\neq 0$, and let $H$ be a real $4\times 4$ matrix. Then the null transverse-traceless projection of $H$ along $(m,l)$ is Lorentz-transverse to $m$: for every row index $i$, the Minkowski contraction of that row against the raised covector $m$ vanishes.
background
This module is the Lorentzian algebraic layer of the QG edge TT decomposition campaign (Wave 4 / W4-1). It specializes the Euclidean TT layer to signature $(-+++)$ on Fin 4, including the physically relevant null wave-covector case. Covectors are lowered by default; raising negates the time component. The Minkowski pairing is $m\cdot m=-(m_0)^2+\sum_{i=1}^3(m_i)^2$.
Lorentz transversality means each row of a covariant matrix contracts to zero against the raised wave covector: $\forall i,; -(H_{i0})m_0+H_{i1}m_1+H_{i2}m_2+H_{i3}m_3=0$. Equivalently, the Lorentz load of $H$ on $m$ vanishes in every component. In the null sector one needs an auxiliary null $l$ with $m\cdot l\neq 0$; the null projector is $P_{ij}=\eta_{ij}-(m_i l_j+l_i m_j)/(m\cdot l)$.
Upstream, lorentzLoad_eq identifies the load with the explicit Minkowski contraction, lorentzLoad_nullProjector_m shows the null projector itself is transverse to $m$, and lorentzLoad_smul / lorentzLoad_sub give linearity of the load.
proof idea
Fix a row index $i$. Rewrite the transversality goal as vanishing of the Lorentz load via lorentzLoad_eq. Invoke two load identities: the companion lemma that the nullPhp contribution loads to zero on $m$, and lorentzLoad_nullProjector_m that the null projector itself loads to zero on $m$. Unfold nullTTProject and apply load linearity (lorentzLoad_sub, lorentzLoad_smul); the two vanishing loads cancel the remaining terms, so the projected matrix is transverse.
why it matters
This is one of the three legs of the algebraic Lorentz TT package in the null sector. Downstream, nullTTProject_isLorentzTT assembles it with the companion symmetry and tracelessness lemmas into the full IsLorentzTT predicate:
⟨nullTTProject_symmetric, nullTTProject_traceless, nullTTProject_transverse_m⟩.
In the Recognition Science gravity lane this sits inside the ledger name edge_tt_decomposition: the Lorentzian linear-algebra layer that prepares transverse-traceless edge data against a Minkowski wave covector. It does not yet touch Regge EDGE perturbations, $S_{\mathrm{RS}}\to EH$ convergence, or gap-action recovery; those are separate campaign targets. The null case is the physically relevant one for radiative / lightlike modes, so closing transversality here is a necessary algebraic step before any polarization or action-level work.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.