sum_nullSMixed_H_col
plain-language theorem explainer
Column contraction of the null mixed projector kernel against a symmetric 4×4 matrix factors into the two Lorentz loads of the auxiliary null pair, each scaled by a covector component over m·l. Gravity analysts cite it when stripping gauge pieces in the null TT layer. The proof expands the mixed kernel termwise, splits the sum, and matches each half to lorentzLoad via symmetry.
Claim. Let $H$ be a symmetric $4\times 4$ real matrix and let $m,l:\{0,1,2,3\}\to\mathbb{R}$ satisfy the Minkowski pairing $m\cdot l\neq 0$. Then for every pair of indices $i,j$, $$\sum_{a} S^{\mathrm{mix}}_{ia}(m,l)\,H_{aj}= m_i\frac{(H\cdot_{\eta} l)_j}{m\cdot l}+ l_i\frac{(H\cdot_{\eta} m)_j}{m\cdot l},$$ where $S^{\mathrm{mix}}$ is the null mixed projector kernel built from $m,l$ and raised indices, and $(H\cdot_{\eta} v)_j$ denotes the Lorentz load of $H$ against the covector $v$.
background
This module is the Lorentzian algebraic layer of the edge TT decomposition campaign (Wave 4 / lane W4-1). It specializes the Euclidean $4\times 4$ TT calculus to signature $(-+++)$, with covectors lowered by default and index raising that negates the time component: $(\mathrm{raise},v)_0=-v_0$ and $(\mathrm{raise},v)_i=v_i$ spatially. The Minkowski pairing is $m\cdot l=\sum_j m_j(\mathrm{raise},l)_j$.
In the null sector one takes an auxiliary covector $l$ with $m\cdot l\neq 0$ and builds the mixed projector kernel whose $(i,a)$-entry is the symmetrized outer product $(m_i l_a+l_i m_a)/(m\cdot l)$ with raised second legs. The Lorentz load of a matrix $H$ against a covector $v$ is the contraction of one index of $H$ with $\mathrm{raise},v$; under symmetry of $H$ the two index placements agree up to commuting the factors.
The ambient objects are plain real $4\times 4$ matrices (Mat4) and the elementary symmetry predicate $H_{ij}=H_{ji}$. No curvature, lattice, or polarization normalization enters at this layer.
proof idea
Set $s:=m\cdot l$ and record $s\neq 0$. For each summation index $a$, unfold the mixed kernel and clear the common denominator to obtain the two-term identity $$S^{\mathrm{mix}}{ia}H{aj}=(m_i/s)(\mathrm{raise},l)a H{aj}+(l_i/s)(\mathrm{raise},m)a H{aj}.$$ Sum over $a$, distribute, and pull the $i$-dependent scalars out of the sums. Each remaining sum $\sum_a(\mathrm{raise},v)a H{aj}$ is rewritten as the Lorentz load of $H$ against $v$ by unfolding that definition, using symmetry $H_{aj}=H_{ja}$, and commuting the product. A final field simplification restores the displayed right-hand side.
why it matters
The identity is the column half of the null gauge subtraction used to define the null gap matrix. Downstream, nullGap_entry writes each entry of that gap as the sum of the two mixed contractions minus the bilinear remainder; this theorem discharges the first of those two sums.
Within the Recognition Science gravity stack it sits in the pure linear-algebra substrate of edge_tt_decomposition. The module explicitly does not yet decompose Regge EDGE perturbations, does not prove convergence of the RS action to Einstein–Hilbert in 4D, and does not flip gap_action_recovery. Closing those ledger names needs exactly this kind of null-projector algebra as a checked lemma, not as a sketch.
No forcing-chain landmark (T5–T8, RCL, eight-tick) is invoked here; the result is metric-linear algebra supporting the later continuum limit arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.