nullTTProject
plain-language theorem explainer
Null transverse-traceless projection of a real 4×4 matrix against a null wave covector with auxiliary null partner. Gravity analysts cite it as the TT residual in the Lorentzian algebraic edge decomposition. Built as the double mixed projection PHP minus half its Minkowski trace times the null projector P.
Claim. For covectors $m,l\in\mathbb{R}^4$ and $H\in M_4(\mathbb{R})$, the null TT projection is $\mathrm{TT}_{m,l}(H)=PHP-\tfrac12\mathrm{tr}_\eta(PHP)\,P$, where $P_{ij}=\eta_{ij}-(m_i l_j+l_i m_j)/(m\cdot l)$ is the null-frame transverse projector and $(PHP)_{ij}=P_i{}^a H_{ab} P_j{}^b$.
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 null case. Signature is $(-,+,+,+)$; covectors are lowered by default; index raising negates the time component. The Minkowski pairing is $m\cdot l=-(m_0)(l_0)+\sum_{i=1}^3 m_i l_i$, and the metric-trace is $\mathrm{tr}\eta H=-H{00}+H_{11}+H_{22}+H_{33}$.
In the null regime $m\cdot m=0$ with $m\neq 0$, one needs an auxiliary null partner $l$ with $m\cdot l\neq 0$. The null projector is $P=\eta-(m\cdot l)^{-1}\mathrm{sym}(m\otimes l)$. The double mixed projection nullPhp is $(PHP){ij}=P_i{}^a H{ab} P_j{}^b$. The scalar nullTraceCoeff is $\mathrm{tr}_\eta(PHP)/2$, the natural screen-trace coefficient in 4D (two transverse directions).
proof idea
Pure definitional abbreviation: subtract the screen-trace multiple of the null projector from the double mixed projection. No tactics, no lemmas applied at the definition site. Downstream lemmas then verify symmetry, Minkowski-tracelessness, and transversality to both $m$ and $l$ under the standing null-frame hypotheses.
why it matters
This is the explicit TT piece in the residual identity of exists_nullLorentzTTDecomposition, the named THEOREM for null Lorentzian algebraic edge TT decomposition: $H=\mathrm{TT}+m$-gauge$+l$-gauge$-$bilinear$+$screen-trace. The companion lemmas nullTTProject_isLorentzTT, _symmetric, _traceless, _transverse_m, and _transverse_m/_l certify that the output lands in the Lorentz TT subspace. Within the Recognition gravity stack this is linear-algebra scaffolding for the ledger name edge_tt_decomposition; it does not yet touch Regge EDGE perturbations, $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$, or gap-action recovery. No direct link to T0–T8 or the RCL; it is pure Minkowski 4D algebra supporting the Clausius–Einstein bridge imports.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.