nullPhp_expand_algebra
plain-language theorem explainer
Algebraic expansion of the double contraction of a 4×4 matrix against two null-projector factors (Kronecker minus mixed null projector) into four separate double sums. Anyone writing the entrywise null-projector formula in the Lorentzian edge TT layer cites this. The proof is pointwise ring expansion, then distributing finite sums over addition and subtraction.
Claim. For covectors $m,\ell:\mathbb{R}^4$, a matrix $H\in M_4(\mathbb{R})$, and indices $i,j\in\{0,1,2,3\}$, $$\sum_{a,b}(\delta_{ia}-S_{ia})H_{ab}(\delta_{jb}-S_{jb})=\sum_{a,b}\delta_{ia}H_{ab}\delta_{jb}-\sum_{a,b}S_{ia}H_{ab}\delta_{jb}-\sum_{a,b}\delta_{ia}H_{ab}S_{jb}+\sum_{a,b}S_{ia}H_{ab}S_{jb},$$ where $S_{ia}=(m_i\,\ell^{\uparrow a}+\ell_i\,m^{\uparrow a})/(m\cdot\ell)$ is the mixed null projector built from $m$ and the raised partner of $\ell$.
background
This module is the Lorentzian algebraic layer of the edge TT decomposition campaign (Wave 4 / W4-1). It treats symmetric $4\times 4$ real matrices against a Minkowski wave covector on $\mathrm{Fin},4$, signature $(-+++)$, including the physically relevant null case. Covectors are lowered by default; index raising negates the time component. The Minkowski pairing is $\mathrm{minkowskiDot}(a,b)=-(a_0)(b_0)+\sum_{k=1}^3 a_k b_k$.
In the null regime one needs an auxiliary null partner $\ell$ with $m\cdot\ell\neq 0$. The mixed projector factor used here is $S_{ia}=(m_i,\ell^{\uparrow a}+\ell_i,m^{\uparrow a})/(m\cdot\ell)$, so the null projector reads $P_{ij}=\eta_{ij}-S_{ij}$ (symmetrized outer form). The Kronecker symbol $\delta_{ia}$ is the usual $1$ on the diagonal and $0$ off it. The object being expanded is the double contraction of $H$ against two such $(\delta-S)$ factors, one on each free index.
The two upstream $H$ cost symbols that appear in the dependency graph are unrelated cost-algebra reparametrizations ($H=J+1$); they are not used in the body of this identity.
proof idea
Fix indices $a,b$ and expand the scalar product $(\delta_{ia}-S_{ia})H_{ab}(\delta_{jb}-S_{jb})$ by the ring tactic: four monomials with the expected signs. Rewrite the double sum by that pointwise identity, then apply the standard finite-sum distribution lemmas for subtraction and addition over $\mathrm{Fin},4\times\mathrm{Fin},4$. No cancellation, no metric identities, and no nullness hypothesis are required.
why it matters
This is the pure bilinear expansion step that lets the entrywise null-projector formula nullPhp_entry rewrite $\mathrm{nullPhp}(m,\ell,H){ij}$ as $H{ij}$ minus the two mixed contractions plus the bilinear remainder. That entry formula is the algebraic core of the null branch of the Lorentzian TT projector on $4\times 4$ matrices.
In the broader Recognition Science gravity stack this sits inside the ledger-closing name edge_tt_decomposition: the Lorentzian specialization of the Euclidean TT layer. It does not itself recover Einstein–Hilbert dynamics or close the gap-action recovery; it only supplies the linear-algebra identity those later steps need when the wave covector is null. Framework landmarks T0–T8 and the RCL are not invoked here; the result is pure Minkowski linear algebra on $\mathrm{Fin},4$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.