nullTTProject_symmetric
plain-language theorem explainer
The null transverse-traceless projection of a symmetric 4×4 real matrix stays symmetric. Lorentzian gravity analysts cite this when packaging the full null TT property for a Minkowski wave covector. The proof expands the projector formula and rewrites with symmetry of the gauge (PHP) piece and of the null projector.
Claim. Let $H$ be a symmetric $4\times 4$ real matrix and let $m,l$ be covectors on $\mathbb{R}^4$. Then the null TT projection of $H$ relative to $m$ and $l$ is symmetric: its $(i,j)$ entry equals its $(j,i)$ entry for all indices.
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; index raising negates the time component.
A matrix is symmetric when $H_{ij}=H_{ji}$ for all indices. 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$, and builds the projector $P_{ij}=\eta_{ij}-(m_i l_j+l_i m_j)/(m\cdot l)$. The null TT projection subtracts a gauge (PHP) piece built from that projector from $H$.
Upstream, symmetry of the gauge piece and of the null projector itself are already established; this lemma only needs to combine them under the projection formula.
proof idea
Pointwise on indices $i,j$: unfold the null TT projection (difference of $H$ and a scalar multiple of the gauge/projector terms), then rewrite the two summands by the already-proved symmetry of the null PHP gauge piece and of the null projector. No new algebraic identity is derived here; it is a short composition of those two symmetry lemmas after simp exposes the matrix entries.
why it matters
This is the symmetry leg of the null TT package. Downstream, nullTTProject_isLorentzTT assembles it with the matching traceless and $m$-transverse lemmas into the full Lorentzian TT predicate for the projected matrix. That predicate is the algebraic core of the ledger name edge_tt_decomposition in the Lorentzian specialization of the Euclidean 4D TT layer.
Within Recognition Science gravity work this sits in the QG full-theory campaign: it supplies the linear-algebra fact needed before any continuum or Regge-edge identification, without yet claiming Einstein-Hilbert recovery or polarization normalizations. It does not touch the forcing chain (T0–T8) or the RCL directly; it is infrastructure for the gravitational side of the ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.