lorentzLoad_nullProjector_m
plain-language theorem explainer
For a null Minkowski covector m and auxiliary l with m·l ≠ 0, the Lorentz load of the null projector P(m,l) against m vanishes componentwise. Anyone building the null transverse-traceless projector on 4×4 symmetric matrices cites this. The proof unfolds P, distributes load over subtraction and scalar multiplication, applies the load identities for η and the symmetrized outer product, then cancels by field_simp and ring.
Claim. Let $m,l:\mathbb{R}^4$ be covectors with Minkowski pairing $m\cdot m=0$ and $m\cdot l\neq 0$. Write $P_{ij}=\eta_{ij}-(m_i l_j+l_i m_j)/(m\cdot l)$ for the null projector. Then for every index $i$, the Lorentz load $(P\cdot m^\sharp)_i$ equals zero.
background
This module is the Lorentzian algebraic layer of the edge TT decomposition campaign (Wave 4 / W4-1): 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 $\mathrm{minkowskiDot},a,b=-(a_0)(b_0)+\sum_{k=1}^3 a_k b_k$. Lorentz load of a matrix $H$ against $m$ is $(H\cdot m^\sharp)i=\sum_j H{ij}(\mathrm{raise},m)_j$, the contraction that defines Lorentz transversality. For null $m$ ($m\cdot m=0$) one needs an auxiliary null $l$ with $m\cdot l\neq 0$; the null projector is $P=\eta-(\mathrm{symmetrized,outer},m,l)/(m\cdot l)$.
Upstream load lemmas already give: load of $\eta$ recovers $m$; load is linear in the matrix; load of the symmetrized outer product $m\odot l$ expands to $(l\cdot m),m+(m\cdot m),l$.
proof idea
Unfold the null projector definition, then rewrite with the four load structural lemmas: load of a difference, load of $\eta$, load of a scalar multiple, and load of the symmetrized outer product. After those rewrites the expression is $m_i - (m\cdot l)^{-1}\bigl((l\cdot m),m_i+(m\cdot m),l_i\bigr)$. Commute $l\cdot m$ to $m\cdot l$, substitute the null hypothesis $m\cdot m=0$, then field_simp on the nonzero denominator $m\cdot l$ and finish by ring.
why it matters
This is the key algebraic identity that makes the null projector Lorentz-transverse to its wave covector. Downstream, nullTTProject_transverse_m applies it (via an intermediate load identity) to prove that the full null TT projection of an arbitrary symmetric matrix is Lorentz-transverse to $m$.
In the Recognition Science gravity stack this sits in the Lorentzian linear-algebra layer of the ledger name edge_tt_decomposition. It does not yet touch Regge edge perturbations, Einstein-Hilbert recovery, or polarization normalizations; it only closes the null-case projector kernel needed before those geometric steps. The Euclidean sibling layer already had the non-null projector; this fills the physically relevant lightlike case under signature $(-+++)$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.