ttProject_traceless
plain-language theorem explainer
The TT projection of a real 4×4 matrix against a non-null Minkowski wave covector has vanishing Minkowski trace. Gravity analysts cite it when packaging the full Lorentz TT projector (symmetry + traceless + transverse). The proof unfolds the projection, rewrites the Minkowski trace through subtraction and scalar-multiplication lemmas, applies the transverse-projector trace identity, and closes by ring.
Claim. Let $m\in\mathbb{R}^4$ satisfy $m\cdot_{\eta} m\neq 0$ and let $H$ be any real $4\times 4$ matrix. Then the transverse-traceless projection of $H$ relative to $m$ is Lorentz-traceless: $\mathrm{tr}_{\eta}(\mathrm{TT}_m(H))=0$, where $\mathrm{tr}_{\eta}H=-(H_{00})+H_{11}+H_{22}+H_{33}$.
background
This module is the Lorentzian algebraic layer of the QG campaign lane edge_tt_decomposition (Wave 4 / W4-1): TT decomposition of symmetric real $4\times 4$ matrices against a Minkowski wave covector on $\mathrm{Fin},4$, signature $(-+++)$. Covectors are lowered by default; raising negates the time component. The Minkowski pairing is $m\cdot_{\eta}n=-(m_0 n_0)+\sum_{i=1}^3 m_i n_i$, and the metric-trace is $\mathrm{tr}{\eta}H=\eta^{ij}H{ij}$.
Lorentz-tracelessness means $\mathrm{tr}{\eta}H=0$. In the non-null sector $m\cdot{\eta}m\neq 0$, the transverse projector is $P_{ij}=\eta_{ij}-m_i m_j/(m\cdot m)$. The TT projection subtracts a residual-trace multiple of that projector from the gauge-corrected matrix, exactly as in the Euclidean sibling EdgeTTDecomposition4D, but with Minkowski trace and pairing throughout.
The Euclidean precursor proves the same claim with Euclidean trace and $m\cdot m\neq 0$ in the flat metric; this declaration is the Lorentzian counterpart.
proof idea
Short tactic proof, parallel to the Euclidean ttProject_traceless. Unfold Lorentz-tracelessness, the TT projection, and the residual-trace scalar. Rewrite the Minkowski trace of a difference and of a scalar multiple (minkowskiTrace_sub, minkowskiTrace_smul), then apply the identity that the transverse projector has Minkowski trace $3$ when $m\cdot_{\eta}m\neq 0$ (minkowskiTrace_transverseProjector). The residual coefficient is defined so the difference cancels; ring finishes.
why it matters
Feeds directly into ttProject_isLorentzTT, which packages symmetry, Lorentz-tracelessness, and Lorentz transversality into the full Lorentz TT predicate for the non-null sector. That parent is the algebraic certificate that the projection lands in the physical TT subspace used by the edge-TT decomposition ledger name.
In the Recognition Science gravity stack this is pure linear algebra on the Lorentzian side of Wave 4: it does not yet touch Regge edge perturbations, $S_{\mathrm{RS}}\to\mathrm{EH}$ convergence, or gap-action recovery. It is the Minkowski twin of the Euclidean tracelessness lemma and is required before polarization counting or null-sector projectors can be trusted in 4D.
No forcing-chain landmark (T0–T8) is at stake here; the result is infrastructure for the Clausius–Einstein / edge-gravity bridge imported by the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.