lorentzLoad_nullProjector_l
plain-language theorem explainer
The null projector built from a pair of Minkowski covectors annihilates its auxiliary null direction under Lorentz load: every component of $(P(m,l)\cdot l^\sharp)$ is zero when $l$ is null and $m\cdot l\neq 0$. Cited by anyone proving Lorentz transversality of the null TT projection. Proof unfolds the projector, applies load-linearity and the symmetrized-outer load identity, then cancels algebraically.
Claim. Let $m,l:\mathbb{R}^{1,3}\to\mathbb{R}$ be covectors with Minkowski pairing $l\cdot l=0$ and $m\cdot l\neq 0$. Write $P(m,l)$ for the null projector $P_{ij}=\eta_{ij}-(m_i l_j+l_i m_j)/(m\cdot l)$. Then for every index $i\in\{0,1,2,3\}$, the Lorentz load vanishes: $(P(m,l)\cdot l^\sharp)_i=0$.
background
This module is the Lorentzian algebraic layer of the edge TT decomposition campaign (Wave 4 / W4-1): 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; index raising flips 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 covariant matrix $H$ against a covector $v$ is the contraction $(H\cdot v^\sharp)i=\sum_j H{ij}(\mathrm{raise},v)j$. In the null regime one takes an auxiliary null $l$ with $m\cdot l\neq 0$ and forms the projector $P{ij}=\eta_{ij}-(m_i l_j+l_i m_j)/(m\cdot l)$.
Upstream load lemmas supply the algebraic toolkit: load of $\eta$ recovers the covector, load is linear in the matrix, and load of the symmetrized outer product $m\odot l$ against $l$ expands to $(l\cdot l)m+(m\cdot l)l$.
proof idea
Term-mode proof by direct expansion. Unfold the null projector into $\eta$ minus a scalar multiple of the symmetrized outer product of $m$ and $l$. Rewrite the load via linearity under subtraction and scalar multiplication, then apply the identity that load of $\eta$ against $l$ is $l$ itself and the outer-product load formula
$$\mathrm{load}(m\odot l,,l)=(l\cdot l),m+(m\cdot l),l.$$
Substitute the hypothesis $l\cdot l=0$. The remaining expression is $l_i-(m\cdot l)^{-1}(m\cdot l),l_i$; field_simp clears the nonzero denominator $m\cdot l$, and ring finishes the cancellation to zero.
why it matters
Feeds the parent theorem nullTTProject_transverse_l, which asserts that the null TT projection of an arbitrary symmetric matrix is Lorentz-transverse to the auxiliary null direction $l$. That transversality step is part of the Lorentzian linear-algebra layer closing the ledger name edge_tt_decomposition.
Within Recognition Science gravity, this is pure algebraic scaffolding for the Clausius–Einstein / edge-mode analysis: it equips the null-wave sector with a projector that kills the gauge direction under load, matching the Euclidean TT layer already present in the sibling module. It does not itself recover Einstein–Hilbert dynamics or flip gap-action recovery; those sit further downstream in the QG campaign. Landmark contact is indirect: the ambient $D=3$ spatial setting (T8) and the four-dimensional Lorentzian signature are the stage on which the null projector acts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.