nullSMixed
plain-language theorem explainer
Defines the mixed-index null gauge kernel S_i{}^a = (m_i l^a + l_i m^a)/(m·l) for two covectors with nonzero Minkowski pairing. Anyone expanding the null TT projector P = I − S, the double projection PHP, or the null gap remainder cites this entry. Pure definitional abbreviation of the raised symmetrized outer product.
Claim. For covectors $m,l:\mathbb{R}^4\to\mathbb{R}$ and indices $i,a\in\{0,1,2,3\}$, set $$S_i{}^{a}(m,l)=\frac{m_i\,l^{a}+l_i\,m^{a}}{m\cdot l},$$ where $v^{a}$ is the raised covector under signature $(-,+,+,+)$ (time component negated) and $m\cdot l$ is the Minkowski pairing $\eta^{ab}m_a l_b$.
background
This module is the Lorentzian algebraic layer of the edge TT decomposition campaign: 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 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{k=1}^3 a_k b_k$, equal to $\sum_j a_j(\mathrm{raise},b)_j$.
In the null regime one takes $m\cdot m=0$, $m\neq 0$, and an auxiliary covector $l$ with $m\cdot l\neq 0$. The projector is then $P_{ij}=\eta_{ij}-(m_i l_j+l_i m_j)/(m\cdot l)$. The present definition is the mixed-index form of that subtracted kernel: $S_i{}^a$ with the second index raised.
proof idea
Definitional one-liner. The body is exactly the raised symmetrized outer product of $m$ and $l$, divided by their Minkowski pairing: $(m_i(\mathrm{raise},l)_a+l_i(\mathrm{raise},m)_a)/(m\cdot l)$. No lemmas are invoked.
why it matters
This is the atomic building block of the null projector algebra. Downstream, nullPMixed is the Kronecker minus this kernel ($P_i{}^a=\delta_i{}^a-S_i{}^a$); nullBilinear is the double contraction $SHS$; and the entrywise identities nullPhp_entry and nullGap_entry expand $PHP$ and the gap remainder as $H-SH-HS+SHS$ written in sums against nullSMixed.
Row and column sum lemmas (sum_H_nullSMixed_row, sum_nullSMixed_H_col, sum_kron_H_S) reduce those contractions to Lorentz loads of $H$ against $m$ and $l$. The whole stack is the Lorentzian specialization of the Euclidean TT layer, feeding the ledger name edge_tt_decomposition without yet touching Regge edge perturbations or $S_{\mathrm{RS}}\to EH$ convergence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.