ttProject
plain-language theorem explainer
Transverse-traceless projection of a real 4×4 matrix against a Euclidean wave covector: subtract the residual pure-trace piece from the gauge-corrected matrix. Gravity and QG workers cite it as the explicit TT summand in the algebraic edge TT decomposition. The body is a one-line linear combination of three sibling operators.
Claim. For a wave covector $m\in\mathbb{R}^4$ and $H\in M_4(\mathbb{R})$, the transverse-traceless projection is $\mathrm{TT}(m,H):=H^{\mathrm{gc}}-\frac{\mathrm{tr}(H^{\mathrm{gc}})}{3}\,P_\perp(m)$, where $H^{\mathrm{gc}}=H-\mathrm{gauge}(m,H)$ is the gauge-corrected matrix and $P_\perp(m)=I-\|m\|^{-2}m\otimes m$ is the Euclidean transverse projector.
background
This module is the algebraic layer of the QG campaign item edge_tt_decomposition (Wave 4 / W4-1): linear-algebra TT decomposition of symmetric real $4\times 4$ matrices against a nonzero Euclidean wave covector on $\mathrm{Fin},4$. Conventions lift the 3D closer chain (Euclidean trace, Euclidean transversality, symmetry) with no Frobenius pin; Minkowski/null specialization is deferred.
Mat4 is $M_4(\mathbb{R})$. The transverse projector is $P_\perp(m)=I-(\sum_i m_i^2)^{-1}(m\otimes m)$. Gauge correction subtracts the pure-gauge piece built from the gauge vector of $H$. Residual trace is the Euclidean trace of that gauge-corrected matrix, scaled by $1/3$, so that subtracting residual-trace times $P_\perp$ kills the remaining isotropic transverse component.
Upstream cost-algebra $H$ (shifted $J$-cost) appears only as a name collision in the dependency graph; the matrix argument here is unrelated to the Recognition Composition Law reparametrization.
proof idea
Pure definition, not a proof. The body is the single matrix expression
gaugeCorrected m H - residualTrace m H • transverseProjector m.
No tactics, no lemmas applied at the definition site. Downstream theorems (ttProject_symmetric, ttProject_traceless, ttProject_transverse, then ttProject_isTT) discharge the three TT conjuncts by unfolding this combination and using the corresponding properties of gauge correction and the transverse projector.
why it matters
This is the explicit TT summand that makes the algebraic decomposition constructive. The parent existence theorem states every symmetric $4\times 4$ matrix against nonzero Euclidean $m$ splits as
$H=\mathrm{TT}(m,H)+\mathrm{gauge}+\beta,P_\perp(m)$ with $\mathrm{IsTT},m,(\mathrm{TT}(m,H))$; the primed form packages the same data as an existential. Certificates ttProject_isTT, ttProject_symmetric, ttProject_traceless, and ttProject_transverse all quote this definition, as do the decoy longitudinal checks that the projector restores transversality.
In the framework it is the smallest kernel-checked increment toward ledger name edge_tt_decomposition. It does not yet touch continuum Einstein–Hilbert recovery or gap-action closure; those remain separate campaign items. Dimension $D=3$ spatial (forcing T8) enters only as the ambient $4=3+1$ index set of the matrices, not as a new forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.