null_gap_expansion
plain-language theorem explainer
Any symmetric real 4×4 matrix H splits as the null PHP projector applied to H plus an explicit residual gap built from the m- and l-gauge pieces (minus the bilinear). Gravity analysts cite it when assembling the null Lorentzian edge TT decomposition. The proof is entrywise: expand both summands and cancel by linear arithmetic.
Claim. Let $H$ be a symmetric $4\times 4$ real matrix and let $m,l:\{0,1,2,3\}\to\mathbb{R}$ be covectors with Minkowski pairing $m\cdot l\neq 0$. Then $H$ equals the null PHP projection of $H$ plus the null residual gap of $H$ against $(m,l)$: $H=\mathrm{PHP}_{m,l}(H)+\mathrm{Gap}_{m,l}(H)$.
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; raising negates the time component. The Minkowski pairing is $m\cdot l=-(m_0)(l_0)+\sum_{i=1}^3 m_i l_i$.
In the null regime one takes an auxiliary partner $l$ with $m\cdot l\neq 0$ and forms the projector $P_{ij}=\eta_{ij}-(m_i l_j+l_i m_j)/(m\cdot l)$. The null PHP piece is the double application of that projector to $H$; the null gap collects the complementary residual (m-gauge + l-gauge − bilinear), matching the doc residual identity $H=\mathrm{PHP}+\text{m-gauge}+\text{l-gauge}-\text{bilinear}$.
Symmetry of $H$ means $H_{ij}=H_{ji}$. The nondegeneracy hypothesis is only $m\cdot l\neq 0$; nullness of $m$ or $l$ is not required at this lemma.
proof idea
Work entrywise via matrix extensionality on indices $i,j$. Invoke the closed-form entry lemmas for the null PHP summand and for the null gap summand (the latter uses symmetry of $H$ and $m\cdot l\neq 0$). Rewrite the sum of matrices componentwise, then finish by linear arithmetic on the resulting real identity. No induction and no spectral argument: pure algebraic cancellation of the residual terms.
why it matters
This residual identity is the bookkeeping step that lets the parent theorem exists_nullLorentzTTDecomposition write a full null Lorentzian algebraic edge TT decomposition: TT projector plus m-gauge plus l-gauge minus bilinear plus screen-trace part. That parent is the named THEOREM for the null case of the ledger closing name edge_tt_decomposition in the QG full-theory campaign.
It sits strictly in the Lorentzian linear-algebra layer: it does not touch Regge EDGE perturbations, does not prove $S_{\mathrm{RS}}$ convergence to Einstein–Hilbert in 4D, and does not flip gap-action recovery. Within Recognition Science gravity analysis it supplies the algebraic scaffold needed before any continuum or polarization normalization is attached.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.