ttProject_traceless
plain-language theorem explainer
The Euclidean TT projection of any real 4×4 matrix against a nonzero wave covector is traceless. Gravity analysts assembling the algebraic edge TT package cite this as one of the three IsTT conjuncts. The argument unfolds the residual-trace correction, uses linearity of Euclidean trace with the fact that the transverse projector has trace three, and finishes by ring.
Claim. Let $m\in\mathbb{R}^{4}$ satisfy $\sum_{i=0}^{3} m_i^2 \neq 0$, and let $H$ be any real $4\times 4$ matrix. Then the Euclidean transverse-traceless projection of $H$ relative to $m$ has vanishing Euclidean trace.
background
This module is the algebraic layer of the QG full-theory campaign lane on edge TT decomposition: the linear-algebra transverse-traceless decomposition of symmetric $4\times 4$ real matrices against a nonzero Euclidean wave covector on $\mathrm{Fin},4$. It lifts the 3D conventions (Euclidean trace, Euclidean transversality, symmetry) without a Frobenius pin, and stops short of Regge EDGE perturbations or continuum Einstein-Hilbert recovery.
A matrix is traceless when its Euclidean trace (sum of diagonal entries) is zero. The squared momentum of a covector $m$ is $\sum_i m_i^2$; the nonzero hypothesis makes the transverse projector well-defined. Upstream, that projector has Euclidean trace exactly 3 (the identity contributes 4, the normalized outer square contributes 1).
The TT projection is built by subtracting a residual-trace multiple of the transverse projector from the input matrix, forcing the output into the traceless slice while retaining the transverse (and, when the input is symmetric, the symmetric) conditions.
proof idea
Short tactic proof. Unfold tracelessness, the TT projection, and the residual-trace scalar. Rewrite Euclidean trace across subtraction and scalar multiplication via the in-module linearity lemmas, then insert the lemma that the transverse projector has Euclidean trace 3 (which consumes the nonzero-momentum hypothesis). The resulting scalar identity is closed by ring.
why it matters
This is one of the three legs of the algebraic IsTT package. The parent theorem that packages the projection as fully TT (symmetric, traceless, and transverse) invokes this result as its middle conjunct, and that package is the kernel-checked increment for the edge_tt_decomposition ledger name in Wave 4 / lane W4-1.
The same Euclidean projector is reused in the Lorentzian companion module: both the Lorentzian TT package and its dedicated tracelessness lemma depend on this statement (or a parallel Minkowski-trace rewrite). Inside Recognition Science gravity analysis it supplies the algebraic TT slice needed before continuum or lattice closing steps. The module doc is explicit that this layer does not yet decompose Regge EDGE perturbations, prove continuum EH recovery in 4D, or flip gap-action recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.