decoy_ttProject_isTT
plain-language theorem explainer
The TT projection of a pure longitudinal decoy (gauge) matrix against the axis wave covector is algebraically transverse-traceless. Gravity analysts cite it when checking that the 4D Euclidean projector kills pure-gauge junk rather than leaving residual longitudinal content. The proof is a one-line application of the general projector-is-TT lemma, feeding symmetry of the decoy and unit momentum-squared of the axis wave.
Claim. Let $m=(1,0,0,0)$ be the axis wave covector on $\mathbb{R}^4$ and let $H$ be the pure gauge (longitudinal decoy) matrix built from $m$ and the vector $v=(1,0,0,0)$. Then the algebraic TT projection of $H$ against $m$ is symmetric, Euclidean-traceless, and transverse to $m$.
background
This module is the algebraic layer of the QG campaign item edge_tt_decomposition: linear-algebra TT decomposition of symmetric real $4\times 4$ matrices against a nonzero Euclidean wave covector on $\mathrm{Fin},4$. It lifts the 3D Euclidean conventions (symmetry, Euclidean trace zero, transversality) without a Frobenius pin; Minkowski/null specialization is deferred.
Algebraic TT means the conjunction of three predicates: the matrix is symmetric, its Euclidean trace vanishes, and it is transverse to the wave covector $m$ (i.e. $H m = 0$). The projector ttProject subtracts the gauge correction and the residual-trace multiple of the transverse projector, so that the output is intended to land in the TT subspace whenever $m$ has nonzero momentum-squared.
The axis wave is the unnormalized covector $(1,0,0,0)$, with momentum-squared equal to $1$. The decoy longitudinal matrix is the pure gauge part of that same axis direction: it is the canonical pure-longitudinal junk one wants the projector to annihilate into a genuine TT (in fact zero) output.
proof idea
One-line term wrapper around the general lemma that ttProject m H is TT whenever $H$ is symmetric and $\mathrm{momentumSq},m\neq 0$. Instantiate at $m=\mathrm{axisWave}$ and $H=\mathrm{decoyLongitudinal}$. Supply the already-proved symmetry of the decoy (inherited from symmetry of every gauge part) and discharge the nonzero-momentum hypothesis by simplifying axisWave_momentumSq, which evaluates to $1$.
why it matters
Feeds the immediate parent decoy_projection_restores_transverse, which unpacks the transverse conjunct of this TT statement: projecting the longitudinal decoy restores transversality to the axis wave. Together these decoy lemmas are the sanity check that the algebraic projector does not leave pure-gauge residue, a necessary kernel step before any claim that every symmetric $4\times 4$ matrix decomposes as TT plus gauge plus transverse-trace part.
In the broader Recognition gravity lane this is Wave 4 / W4-1 scaffolding for edge TT structure on 4D lattices. It does not yet touch continuum Lorentzian polarizations, Regge edge perturbations, or the action-recovery gap; it only certifies the Euclidean linear-algebra kernel that those later steps will quote. The two independent axis TT polarizations (plus and cross) live in the same file and rely on the same projector infrastructure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.