ttProject_isTT
plain-language theorem explainer
The algebraic TT projector applied to any symmetric 4×4 real matrix against a nonzero Euclidean wave covector lands in the transverse-traceless subspace. Gravity and continuum-limit workers cite it when assembling the edge TT decomposition. The proof is a three-conjunct constructor from the projector’s symmetry, tracelessness, and transversality lemmas.
Claim. Let $H$ be a symmetric $4\times 4$ real matrix and $m\in\mathbb{R}^4$ a covector with nonzero Euclidean squared norm. Then the algebraic TT projection of $H$ along $m$ is symmetric, Euclidean-traceless, and transverse to $m$.
background
This module is the algebraic layer of the QG campaign lane edge_tt_decomposition: linear-algebra TT decomposition of symmetric $4\times 4$ 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; Minkowski/null specialization is deferred.
Mat4 is simply $\mathrm{Matrix}(\mathrm{Fin},4,\mathrm{Fin},4,\mathbb{R})$. Algebraic TT means the conjunction of three properties: matrix symmetry ($H_{ij}=H_{ji}$), vanishing Euclidean trace, and transversality to the wave covector $m$. The squared-momentum hypothesis $m\cdot m\neq 0$ keeps the projectors well-defined.
The local goal is only the kernel-checked linear algebra; the module doc explicitly does not claim Regge EDGE perturbation decomposition, $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$ convergence, or gap-action recovery.
proof idea
Term-mode proof: package the three conjuncts of IsTT as an anonymous constructor. Symmetry of the projected matrix is ttProject_symmetric (uses only symmetry of $H$). Tracelessness and transversality are ttProject_traceless and ttProject_transverse, both needing the nonzero squared-momentum hypothesis so the Euclidean projectors divide cleanly. No further rewriting or case splits.
why it matters
Feeds the main existence theorem exists_edgeTTDecomposition, which states every symmetric $4\times 4$ matrix against nonzero Euclidean $m$ splits as TT + gauge + transverse-trace residual, and whose second conjunct is exactly this result. Also used by the decoy sanity check decoy_ttProject_isTT on an axis wave vector.
In the Recognition gravity stack this is the algebraic kernel of the edge TT decomposition layer (Wave 4 / W4-1). It does not yet close continuum Einstein–Hilbert recovery or the gap-action flag; those sit upstream of the forcing chain’s geometric landmarks (eight-tick octave, $D=3$) and remain out of scope here. The declaration earns its place by making the TT summand of the decomposition a proved object rather than a hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.