nullPhp_lorentzLoad_l
plain-language theorem explainer
If l is a null covector and m·l ≠ 0, the Lorentz load of the null-projected matrix nullPhp(m,l,H) against l vanishes componentwise. Gravity analysts building the Lorentzian edge TT projector cite this to get l-transversality of the projected strain. The proof unfolds the load and projector, reorders finite sums, and kills each summand by the mixed-projector contraction identity against raise(l).
Claim. Let $m,l:\mathbb{R}^{4}$ be covectors and $H$ a real $4\times 4$ matrix. Assume the Minkowski pairing satisfies $l\cdot l=0$ and $m\cdot l\neq 0$. Then for every index $i\in\{0,1,2,3\}$, the Lorentz load of the null-projected matrix $P^{\mathrm{null}}(m,l)H$ against $l$ vanishes: $\bigl((P^{\mathrm{null}}(m,l)H)\cdot l^{\sharp}\bigr)_{i}=0$.
background
This module is the Lorentzian algebraic layer of the edge TT decomposition campaign (Wave 4 / W4-1). Signature is $(-,+,+,+)$ on Fin 4. Covectors are lowered by default; index raising negates the time slot, so (raise v) 0 = -v 0 and is the identity on spatial slots. The Minkowski pairing is $\eta^{ij}a_i b_j$, written minkowskiDot, and equals $\sum_j a_j,(\mathrm{raise},b)_j$.
Lorentz load is the contraction $(H\cdot m^{\sharp})i=\sum_j H{ij},(\mathrm{raise},m)j$. Transversality means that load vanishes for every row. In the null sector one takes an auxiliary null covector $l$ with $m\cdot l\neq 0$ and forms the null projector $P{ij}=\eta_{ij}-(m_i l_j+l_i m_j)/(m\cdot l)$. The operator nullPhp applies that projector (via the mixed kernel nullPMixed) to a symmetric matrix $H$.
The present lemma is the load-vanishing identity that turns the algebraic projector into an $l$-transverse matrix. It sits strictly inside the linear-algebra layer: no Regge edge dynamics, no continuum EH limit, no polarization normalization.
proof idea
Unfold lorentzLoad and nullPhp to a double sum of nullPMixed factors times $H_{ab}$ contracted against raise l. Establish a sum-swap identity hswap by rewriting with Finset.sum_mul / Finset.mul_sum, associating multiplications, commuting the outer sum, and commuting the inner pair of sums. After rw [hswap], the expression is a double sum over $a,b$ of a prefactor times $\sum_j \mathrm{nullPMixed}(m,l)_{jb},(\mathrm{raise},l)_j$. Each inner sum vanishes by the already-proved contraction lemma sum_nullPMixed_raise_l (using $l\cdot l=0$ and $m\cdot l\neq 0$), so Finset.sum_eq_zero twice finishes the goal.
why it matters
This is the load kernel for null-sector transversality in the Lorentzian TT layer. Downstream, nullPhp_transverse_l is a one-line rewrite through lorentzLoad_eq that quotes this identity at every index, establishing IsLorentzTransverse l (nullPhp m l H). The full null TT projector then inherits the same $l$-transversality in nullTTProject_transverse_l, which again opens by invoking this lemma.
In the Recognition Science gravity stack this closes the algebraic half of ledger name edge_tt_decomposition for null wave covectors (the physically relevant lightlike case). It does not touch the Euclidean twin, the continuum recovery S_RS_converges_EH_4d, or gap_action_recovery. Framework landmarks T7/T8 (eight-tick octave, $D=3$) sit upstream of the 4D setup; this lemma is pure Minkowski linear algebra feeding those later geometric claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.