nullProjector
plain-language theorem explainer
Null-frame transverse projector for a null covector m with auxiliary null partner l: Minkowski metric minus the normalized symmetrized outer product of m and l. Cited by anyone building the Lorentzian algebraic edge TT decomposition in the null sector. One-line definitional assembly of η, the Minkowski pairing inverse, and the symmetrized outer product.
Claim. For covectors $m,\ell\in\mathbb{R}^4$, define the null transverse projector $P(m,\ell):=\eta-\frac{1}{m\cdot\ell}\,(m\otimes\ell+\ell\otimes m)$ as a real $4\times 4$ matrix, where $\eta$ is the Minkowski metric of signature $(-+++)$ and $m\cdot\ell$ is the Minkowski pairing.
background
This module is the Lorentzian algebraic layer of the QG campaign lane edge_tt_decomposition: transverse-traceless splitting 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 $\mathrm{minkowskiDot}(a,b)=-(a_0)(b_0)+\sum_{i=1}^3 a_i b_i$, and $\mathrm{minkowskiEta}$ is the corresponding metric matrix.
For non-null $m$ the projector is $\eta_{ij}-m_i m_j/(m\cdot m)$. In the null case $m\cdot m=0$ with $m\neq 0$, one needs an auxiliary null $\ell$ with $m\cdot\ell\neq 0$; the projector becomes $\eta_{ij}-(m_i\ell_j+\ell_i m_j)/(m\cdot\ell)$. The sibling $\mathrm{symmetrizedOuter}(m,\ell)_{ij}=m_i\ell_j+\ell_i m_j$ packages that bilinear piece. $\mathrm{Mat4}$ is just $\mathrm{Matrix}(\mathrm{Fin},4)(\mathrm{Fin},4),\mathbb{R}$.
proof idea
Pure definition: subtract the scalar multiple $(m\cdot\ell)^{-1}$ of the symmetrized outer product of $m$ and $\ell$ from the Minkowski metric matrix. No lemmas, no tactics; the formula is the content. Downstream lemmas unfold this def and rewrite with load/trace/symmetry identities for $\eta$ and the outer product.
why it matters
This is the algebraic projector that makes the null Lorentzian TT decomposition work. It is the building block of $\mathrm{nullTTProject}$ (subtract the screen-trace part along $P$), and of the residual identity $\mathrm{exists_nullLorentzTTDecomposition}$: every symmetric $H$ splits as null-TT plus $m$-gauge plus $\ell$-gauge minus bilinear plus screen-trace. Supporting lemmas prove $P$ is symmetric, has Minkowski trace $2$, and is transverse to both raised null directions ($\mathrm{lorentzLoad},P,m=0$ and $\mathrm{lorentzLoad},P,\ell=0$ under the null hypotheses). It closes the null half of the Lorentzian linear-algebra layer for ledger name $\mathrm{edge_tt_decomposition}$; it does not itself decompose Regge edge perturbations or recover the Einstein-Hilbert action.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.