nullProjector_symmetric
plain-language theorem explainer
The null-frame transverse projector built from a null covector m and auxiliary null l is a symmetric 4×4 matrix. Anyone assembling Lorentzian TT projections of symmetric tensors cites this. The proof is a two-line rewrite: both the Minkowski metric and the symmetrized outer product are already symmetric, so their linear combination is.
Claim. For any covectors $m,l:\mathbb{R}^4\to\mathbb{R}$, the null transverse projector $P_{ij}=\eta_{ij}-(m\cdot l)^{-1}(m_i l_j+l_i m_j)$ is symmetric: $P_{ij}=P_{ji}$ for all indices $i,j\in\{0,1,2,3\}$.
background
This module is the Lorentzian algebraic layer of the edge TT decomposition campaign (Wave 4 / W4-1). It specializes the Euclidean 4×4 TT layer to signature $(-+++)$, with covectors lowered by default and index raising that negates the time component. The Minkowski metric $\eta$ and pairing $m\cdot l$ are the ambient structures.
For a null wave covector $m$ ($m\cdot m=0$, $m\neq 0$) one needs an auxiliary null $l$ with $m\cdot l\neq 0$. The null transverse projector is then $P=\eta-(m\cdot l)^{-1},\mathrm{sym}(m\otimes l)$, where $\mathrm{sym}(m\otimes l){ij}=m_i l_j+l_i m_j$. Symmetry of matrices means $H{ij}=H_{ji}$ on $\mathrm{Fin},4$.
Upstream, minkowskiEta_symmetric already records $\eta_{ij}=\eta_{ji}$, and symmetrizedOuter_symmetric records that the symmetrized outer product is symmetric by a ring identity.
proof idea
Term-style proof by unfolding. Fix indices $i,j$. Unfold the definition of the null projector to $\eta-(m\cdot l)^{-1},\mathrm{sym}(m\otimes l)$. After simplifying scalar multiplications and subtraction pointwise, rewrite the two summands by the already-proved facts that $\eta$ is symmetric and that the symmetrized outer product is symmetric. Equality of the swapped indices follows immediately.
why it matters
Null projectors are the physically relevant case for lightlike edge modes in the Lorentzian TT layer. Downstream, nullTTProject_symmetric uses this lemma (together with symmetry of the null PHP correction) to conclude that the full null TT projection of a symmetric matrix remains symmetric. That closes a necessary algebraic gate before any claim that the projected residual is Lorentz-transverse and traceless.
In the Recognition Science gravity stack this sits inside the ledger name edge_tt_decomposition: pure linear algebra on $4\times 4$ matrices against a Minkowski wave covector. It does not yet touch Regge EDGE perturbations, $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$ convergence, or gap-action recovery. It is a proved building block, not scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.