sum_H_nullSMixed_row
plain-language theorem explainer
Row contraction of a 4×4 matrix against the mixed null symmetrizer factors into two Lorentz-load terms weighted by the auxiliary null covectors. Used when assembling the null TT gap matrix entry. Proof expands the mixed kernel termwise, distributes the sum, and matches the load definition.
Claim. Let $m,l\in\mathbb{R}^4$ with Minkowski pairing $m\cdot l\neq 0$, let $H$ be a real $4\times 4$ matrix, and fix indices $i,j\in\{0,1,2,3\}$. Then $\sum_b H_{ib}\,S^{\mathrm{mix}}_{jb}(m,l)=m_j\frac{(H\cdot l^\sharp)_i}{m\cdot l}+l_j\frac{(H\cdot m^\sharp)_i}{m\cdot l}$, where $S^{\mathrm{mix}}_{ja}=(m_j l^a+l_j m^a)/(m\cdot l)$ and $v^\sharp$ is index raising for signature $(-+++)$.
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$ matrices against a Minkowski wave covector on $\mathrm{Fin},4$, including the null case. Signature is $(-+++)$; covectors are lowered by default. Index raising negates the time component. The Minkowski pairing is $m\cdot l=\eta^{ab}m_a l_b=\sum_j m_j(\mathrm{raise},l)_j$.
In the null regime one takes $m\cdot m=0$ with $m\neq 0$ and an auxiliary null $l$ satisfying $m\cdot l\neq 0$. The mixed projector kernel is $S^{\mathrm{mix}}_{ia}=(m_i l^a+l_i m^a)/(m\cdot l)$. The Lorentz load $(H\cdot m^\sharp)i=\sum_j H{ij}(\mathrm{raise},m)_j$ is the natural contraction of a covariant matrix row against a raised covector. This lemma isolates the pure row half of that contraction against $S^{\mathrm{mix}}$.
proof idea
Set $s:=m\cdot l$ and use $s\neq 0$. For each summand $b$, unfold the mixed kernel and apply field simplification plus ring to rewrite
$H_{ib}S^{\mathrm{mix}}{jb}=(m_j/s),H{ib}l^b+(l_j/s),H_{ib}m^b$.
Rewrite the sum with that identity, split by sum_add_distrib, pull the $j$-dependent scalars out with mul_sum, unfold the Lorentz-load definition on each remaining sum, and clear the common denominator $s$ by field simplification. No external lemmas beyond the local defs are required.
why it matters
Feeds nullGap_entry, which expands the null gap matrix as the sum of the two mixed contractions minus the bilinear remainder. That identity is the algebraic engine for the null branch of the Lorentzian TT projector: without factoring the row (and the dual column) sums, the gap cannot be matched to the gauge outer-product terms. Within the QG full-theory campaign this sits in the linear-algebra layer of edge_tt_decomposition; it does not yet touch Regge edge perturbations or $S_{\mathrm{RS}}\to EH$ convergence. Landmark contact is indirect: the eight-tick / $D=3$ forcing chain motivates 4D Lorentzian kinematics, but this lemma is pure Minkowski matrix algebra.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.