sum_nullSMixed_raise_m
plain-language theorem explainer
When the wave covector m is null and paired nontrivially with an auxiliary null covector l, the mixed null projector kernel S contracts against the raised m to recover raised m itself: ∑_j S_{jb} m^j = m^b. Gravity analysts building the Lorentzian edge TT decomposition cite it to show the gauge/mixed piece acts as the identity on the null direction. The proof expands S, splits the sum, and cancels via m·m = 0 and the Minkowski sum identity.
Claim. Let $m,l:\mathbb{R}^4\to\mathbb{R}$ be covectors with Minkowski pairing $m\cdot m=0$ and $m\cdot l\neq 0$. Write $S_{ib}=(m_i l^a+l_i m^a)/(m\cdot l)$ for the mixed null kernel (indices raised by the $(-,+,+,+)$ metric). Then for every index $b$, $\sum_{j=0}^{3} S_{jb}\, m^j = m^b$.
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 negates the time component: $(\mathrm{raise},v)0=-v_0$ and equals $v_i$ spatially. The Minkowski pairing is $\eta^{ij}a_i b_j=-(a_0)(b_0)+\sum{k=1}^{3}a_k b_k$, equivalently $\sum_j a_j(\mathrm{raise},b)_j$.
For null $m$ ($m\cdot m=0$, $m\neq 0$) one introduces an auxiliary $l$ with $m\cdot l\neq 0$ and builds the projector $P_{ij}=\eta_{ij}-(m_i l_j+l_i m_j)/(m\cdot l)$. The mixed kernel $S$ is exactly that subtracted bilinears piece: $S_{ia}=(m_i l^a+l_i m^a)/(m\cdot l)$. The identity here says $S$ acts as the identity when contracted on the first index against raised $m$.
proof idea
Set $s:=m\cdot l\neq 0$. For each $j$, unfold $S_{jb}$ and clear the denominator to rewrite the summand as $(l^b/s)(m_j m^j)+(m^b/s)(l_j m^j)$. Sum over $j$, distribute, and pull out the $b$-dependent coefficients. Replace the two inner sums by Minkowski pairings via $\mathrm{minkowskiDot_eq_sum}$. The first pairing is $m\cdot m=0$ by hypothesis; the second is $l\cdot m$, rewritten as $m\cdot l$ by commutativity. Field simplification then yields $m^b$.
why it matters
Feeds immediately into $\mathrm{sum_nullPMixed_raise_m}$, which shows the full null projector $P=\eta-S$ annihilates raised $m$: $\sum_j P_{jb} m^j=0$. That transversality identity is the algebraic heart of the null Lorentzian TT projector used throughout the edge TT decomposition lane. The module is the Lorentzian specialization of the Euclidean algebraic TT layer; it closes the linear-algebra half of the ledger name $\mathrm{edge_tt_decomposition}$ without yet decomposing Regge edge perturbations or recovering the Einstein–Hilbert continuum limit. Within Recognition Science gravity, this is pure Minkowski linear algebra supporting the Clausius–Einstein bridge imports, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.