nullProjector_minkowskiTrace
plain-language theorem explainer
The Minkowski metric-trace of the null projector built from covectors m and l with nonzero pairing equals 2. Cited by anyone assembling the Lorentzian transverse-traceless projection of a symmetric 4×4 matrix against a null wave covector. Proof unfolds the projector and reduces by linearity of the metric-trace plus the known traces of η and the symmetrized outer product.
Claim. Let $m,l\in\mathbb{R}^{4}$ be covectors with Minkowski pairing $m\cdot l\neq 0$. The null projector $P_{ij}=\eta_{ij}-(m_i l_j+l_i m_j)/(m\cdot l)$ has metric-trace $\eta^{ij}P_{ij}=2$.
background
This module is the Lorentzian algebraic layer of the QG campaign lane edge_tt_decomposition (Wave 4 / W4-1): transverse-traceless decomposition of symmetric real $4\times 4$ matrices against a Minkowski wave covector on $\mathrm{Fin},4$, including the 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 the metric-trace of a covariant matrix is $\mathrm{minkowskiTrace}(H)=-(H_{00})+H_{11}+H_{22}+H_{33}$.
For a null wave covector $m$ ($m\cdot m=0$, $m\neq 0$) one introduces an auxiliary null $l$ with $m\cdot l\neq 0$. The null projector is then $P=\eta-(m\otimes_s l)/(m\cdot l)$, where $m\otimes_s l$ is the symmetrized outer product. Upstream lemmas record that $\mathrm{minkowskiTrace}(\eta)=4$, that the metric-trace is linear (homogeneous under scalar multiplication and additive under subtraction), and that $\mathrm{minkowskiTrace}(m\otimes_s l)=2,m\cdot l$.
proof idea
Term-mode proof. Unfold the definition of the null projector (difference of $\eta$ and a scalar multiple of the symmetrized outer product). Rewrite the metric-trace through the four algebraic lemmas: additivity under subtraction, homogeneity under scalar multiplication, $\mathrm{minkowskiTrace}(\eta)=4$, and $\mathrm{minkowskiTrace}(m\otimes_s l)=2,m\cdot l$. The resulting rational expression simplifies by field_simp using $m\cdot l\neq 0$, then ring yields $4-2=2$.
why it matters
Feeds the single downstream consumer nullTTProject_traceless, which shows that the null TT projection of a symmetric matrix is Lorentz-traceless: after subtracting the appropriate multiple of the null projector, the metric-trace vanishes precisely because that projector contributes trace 2. Without this identity the null branch of the Lorentzian TT decomposition cannot close the tracelessness obligation.
In the Recognition Science gravity stack this is pure 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}$ convergence, or gap-action recovery; those sit further downstream. The result is the null-case counterpart of the non-null projector trace (which equals 3), fixing the coefficient that removes the pure-trace gauge piece when the wave covector is lightlike.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.