lorentzLoad_transverseProjector
plain-language theorem explainer
For any non-null Minkowski covector m, the Lorentz load of the transverse projector P(m) against m vanishes componentwise. Gravity and QG analysts cite this when verifying that the non-null TT projector is transverse. The proof unfolds P, applies load-linearity lemmas, and cancels by field simplification and ring.
Claim. Let $m \in \mathbb{R}^{4}$ satisfy $m \cdot m \neq 0$ in the Minkowski pairing of signature $(-+++)$. Write $P(m)_{ij} = \eta_{ij} - m_i m_j/(m\cdot m)$ for the transverse projector. Then for every index $i$, $(P(m)\cdot m^{\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 null case. Signature is $(-+++)$; covectors are lowered by default; raising negates the time component.
The Lorentz load of a matrix $H$ against $m$ is the covector $(H\cdot m^{\sharp}){i} = \sum_j H{ij},(\mathrm{raise},m){j}$. Lorentz transversality is exactly the vanishing of this load. For non-null $m$ the transverse projector is $P{ij}=\eta_{ij}-m_i m_j/(m\cdot m)$, the Lorentzian analogue of the Euclidean projector in EdgeTTDecomposition4D.
Upstream, load is linear in the matrix argument (lorentzLoad_sub, lorentzLoad_smul), recovers $m$ on the metric (lorentzLoad_eta), and multiplies by $m\cdot m$ on the outer square (lorentzLoad_outerSq). Those four identities are the only algebraic fuel needed here.
proof idea
Unfold the definition $P(m)=\eta-(m\cdot m)^{-1}\cdot(m\otimes m)$. Rewrite the load of a difference via lorentzLoad_sub, then apply lorentzLoad_eta, lorentzLoad_smul, and lorentzLoad_outerSq in turn. The resulting expression is $m_i - (m\cdot m)^{-1}\cdot(m\cdot m),m_i$. With the non-null hypothesis, field_simp clears the denominator and ring cancels to zero.
why it matters
Transversality of the non-null projector is the first structural check before any TT claim. Downstream, ttProject_transverse uses this identity (via the gauge-corrected intermediate) to prove that the full TT projection of an arbitrary symmetric matrix is Lorentz-transverse.
In the Recognition Science gravity stack this sits in the linear-algebra substrate of ledger name edge_tt_decomposition. It does not yet touch Regge edge perturbations, Einstein-Hilbert recovery, or polarization normalizations; those are explicitly out of scope for the module. Closing this algebraic gate keeps the Lorentzian TT lane free of sorry and ready for the geometric layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.