sum_nullPMixed_raise_m
plain-language theorem explainer
For a null Minkowski covector m and auxiliary null l with m·l ≠ 0, the mixed null projector P contracts against the raised m to zero on every column: ∑_j P_j{}^b m^j = 0. Gravity and GR analysts cite it when checking that the null TT projector is transverse to the wave covector. The proof unfolds P = δ − S, collapses the Kronecker sum, and cancels against the companion identity for S.
Claim. Let $m,l:\mathbb{R}^{1,3}\to\mathbb{R}$ be covectors with $m\cdot m=0$ and $m\cdot l\neq 0$. Write $P_j{}^{b}=\delta_j^{b}-S_j{}^{b}$ for the mixed null projector built from $m$ and $l$, and let $m^{j}$ be the index-raised components of $m$. Then for every column index $b\in\{0,1,2,3\}$, $$\sum_{j=0}^{3} P_j{}^{b}\, m^{j}=0.$$
background
This module is the Lorentzian algebraic layer of the edge TT decomposition campaign (Wave 4 / W4-1). Signature is $(-,+,+,+)$; covectors are lowered by default. Index raising negates the time slot: $(\mathrm{raise},v)_0=-v_0$ and $(\mathrm{raise},v)i=v_i$ spatially. The Minkowski pairing is $\mathrm{minkowskiDot}(a,b)=-(a_0)(b_0)+\sum{i=1}^{3}a_i b_i$, equal to $\sum_j a_j(\mathrm{raise},b)_j$.
In the null case $m\cdot m=0$ one needs an auxiliary covector $l$ with $m\cdot l\neq 0$. The mixed null projector is $P_i{}^{a}=\delta_i^{a}-S_i{}^{a}$, where $S$ is the symmetrized outer contribution $(m_i l^{a}+l_i m^{a})/(m\cdot l)$ (encoded as nullSMixed). The companion lemma sum_nullSMixed_raise_m states that $\sum_j S_j{}^{b} m^j=m^b$ whenever $m$ is null. The present result is the corresponding identity for $P$ itself: $P$ annihilates the raised wave covector.
proof idea
Unfold $P=\delta-S$ and split the sum into a Kronecker piece minus the $S$ piece. Symmetry of the Kronecker symbol reduces $\sum_j \delta_j^{b} m^j$ to $m^b$ via sum_kron_left. The $S$ sum is exactly sum_nullSMixed_raise_m, which equals $m^b$ under the null hypotheses. Subtract and cancel by ring.
why it matters
Transversality of the null projector is the algebraic reason the double-projected strain nullPhp m l H is Lorentz-transverse to $m$. The sole downstream consumer is nullPhp_lorentzLoad_m, which proves $\mathrm{lorentzLoad}(\mathrm{nullPhp},m,l,H,m)_i=0$. That step is required for the null branch of the Lorentzian TT decomposition: after gauge stripping, the residual is both traceless and transverse to the null wave covector.
Within the QG full-theory campaign this sits in the pure linear-algebra layer of edge_tt_decomposition. It does not yet touch Regge edge perturbations, the continuum limit $S_{\mathrm{RS}}\to S_{\mathrm{EH}}$, or polarization normalizations. It is the null analogue of the non-null projector identity that kills $m$ against $P_{ij}=\eta_{ij}-m_i m_j/(m\cdot m)$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.