nullGap_entry
plain-language theorem explainer
Entrywise expansion of the null-case residual (gap) for a symmetric 4×4 real matrix against a pair of Minkowski covectors with nonzero pairing. Gravity analysts in the Lorentzian edge TT layer cite it to open the residual identity H = PHP + gap. Unfolds the gap into gauge vectors, rewrites the two mixed sums by dedicated column/row lemmas, and closes by ring.
Claim. Let $H$ be a symmetric $4\times 4$ real matrix and let $m,l:\{0,1,2,3\}\to\mathbb{R}$ satisfy $m\cdot l\neq 0$ in the Minkowski pairing of signature $(-+++)$. For every index pair $(i,j)$, the $(i,j)$-entry of the null gap of $H$ equals $\sum_a S^{\mathrm{mix}}_{ia}H_{aj}+\sum_b H_{ib}S^{\mathrm{mix}}_{jb}-B_{ij}$, where $S^{\mathrm{mix}}$ is the mixed null kernel built from $m,l$ and $B$ is the null bilinear correction.
background
The module is the Lorentzian algebraic layer of the QG campaign lane edge_tt_decomposition: transverse-traceless decomposition 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; raising negates the time component. The Minkowski pairing is $m\cdot l=-(m_0)(l_0)+\sum_{k=1}^3 m_k l_k$, and the metric-trace is $\eta^{ij}H_{ij}=-(H_{00})+H_{11}+H_{22}+H_{33}$.
In the null regime one takes $m\cdot m=0$ with $m\neq 0$ and an auxiliary null $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 null gap packages the $m$-gauge, $l$-gauge, and bilinear correction left after the projected PHP piece is removed. Symmetry of $H$ ($H_{ij}=H_{ji}$) is required so those gauge pieces assemble into a symmetric residual matrix.
proof idea
Short term proof. Unfold the null gap together with its gauge constituents (the gauge part and the two null gauge vectors built from $m$ and $l$). Simplify matrix addition and subtraction pointwise. Rewrite the column mixed sum by sum_nullSMixed_H_col (which uses symmetry of $H$) and the row mixed sum by sum_H_nullSMixed_row. Close with ring to match the target combination of the two mixed sums minus the bilinear term.
why it matters
Direct input to null_gap_expansion, whose doc-comment states the residual identity $H=\mathrm{PHP}+m$-gauge$+l$-gauge$-$bilinear. That identity is the explicit bookkeeping step for the null Lorentzian TT split and is the algebraic core of Wave 4 / lane W4-1 (edge_tt_decomposition) in the QG full-theory campaign. The module is deliberately linear-algebra only: it does not decompose Regge EDGE perturbations on a 4D lattice, does not prove $S_{\mathrm{RS}}$ converges to Einstein-Hilbert in 4d, and attaches no physical polarization normalization. Within Recognition Science this sits on the gravity ledger side, not on the forcing chain T0-T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.