nullTTProject_traceless
plain-language theorem explainer
The null TT projection of any 4×4 real matrix against covectors m,l with nonzero Minkowski pairing is Lorentz-traceless (vanishing metric trace). Gravity analysts assembling the Lorentzian edge TT package cite this as one of the three TT legs. The proof is a short ring cancellation after expanding the metric trace of the projected matrix via the known trace of the null projector.
Claim. Let $m,l\in\mathbb{R}^{4}$ satisfy $m\cdot_{\eta} l\neq 0$, and let $H$ be any real $4\times 4$ matrix. Then the null transverse-traceless projection of $H$ relative to the pair $(m,l)$ has vanishing Minkowski trace: $\eta^{ij}(\mathrm{nullTT}_{m,l}H)_{ij}=0$.
background
This module is the Lorentzian algebraic layer of the QG campaign lane edge_tt_decomposition: transverse-traceless decomposition of symmetric $4\times 4$ real matrices against a Minkowski wave covector on $\mathrm{Fin},4$, including the physically relevant null case. Signature is $(-+++)$. Covectors are lowered by default; the Minkowski pairing is $m\cdot_{\eta} l=-(m_0)(l_0)+\sum_{i=1}^{3}m_i l_i$, and the metric trace of a covariant matrix is $\mathrm{tr}{\eta}H=-(H{00})+H_{11}+H_{22}+H_{33}$.
Lorentz-tracelessness is exactly $\mathrm{tr}{\eta}H=0$. In the null regime one has $m\cdot{\eta}m=0$ with $m\neq 0$, and an auxiliary null covector $l$ obeying $m\cdot_{\eta}l\neq 0$. The null projector is $P_{ij}=\eta_{ij}-(m_i l_j+l_i m_j)/(m\cdot l)$. The null TT projection subtracts a scalar multiple (the null trace coefficient) of a projector-built correction so that the result is intended to be traceless and transverse.
Upstream, metric-trace is linear under scalar multiplication and subtraction (minkowskiTrace_smul, minkowskiTrace_sub), and the null projector itself has a known metric trace (nullProjector_minkowskiTrace) once $m\cdot_{\eta}l\neq 0$.
proof idea
Term-mode proof by direct expansion. Unfold Lorentz-tracelessness, the null TT projection, and the null trace coefficient, so the goal is that the metric trace of $H$ minus a scalar times a projector correction vanishes. Rewrite with linearity of the metric trace under subtraction and scalar multiplication, then replace the projector contribution by nullProjector_minkowskiTrace (which uses $m\cdot_{\eta}l\neq 0$). The remaining scalar identity is discharged by ring.
why it matters
One of the three legs of the full Lorentz-TT package for the null projector. Downstream, nullTTProject_isLorentzTT assembles symmetry, this tracelessness lemma, and null transversality into the single predicate "is Lorentz TT relative to $m$". That package is the algebraic core of the Lorentzian specialization of the Euclidean edge TT layer, under the binding tier that every named result here is a kernel-checked theorem with no sorry.
In the broader Recognition gravity stack this sits in Wave 4 / lane W4-1 (edge_tt_decomposition). It does not itself recover Einstein-Hilbert continuum limits or close gap-action recovery; it only supplies the linear-algebra fact that the null projection lands in the traceless slice, which any later continuum or Regge matching argument will need when polarizations are extracted against a null wave covector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.