decoy_projection_restores_transverse
plain-language theorem explainer
The TT projector applied to a pure longitudinal decoy on the axis wave covector returns a transverse matrix. Gravity analysts cite this as a sanity check that gauge junk is killed by the algebraic edge TT map in 4D. The proof is a one-line projection of the already-proved IsTT triple for that same decoy.
Claim. Let $m=(1,0,0,0)$ be the axis wave covector and let $H$ be the pure gauge (longitudinal) decoy built from $m$. Then the algebraic TT projection of $H$ against $m$ is transverse: for every row index $i$, $\sum_j (\mathrm{ttProject}(m,H))_{ij}\, m_j = 0$.
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$. Conventions lift the 3D chain (Euclidean trace, Euclidean transversality, symmetry) with no Frobenius pin; Lorentzian specialization is deferred.
Transversality means $H m = 0$ row-wise: $\forall i,;\sum_j H_{ij} m_j = 0$. Algebraic TT is the conjunction of symmetry, Euclidean tracelessness, and transversality. The projector is $\mathrm{ttProject}(m,H) = \mathrm{gaugeCorrected}(m,H) - \mathrm{residualTrace}(m,H),\mathrm{transverseProjector}(m)$.
The decoy is the pure gauge piece $\mathrm{gaugePart}(m,v)$ for $v=(1,0,0,0)$ on the fixed axis wave $m=(1,0,0,0)$. Upstream, decoy_ttProject_isTT already shows that $\mathrm{ttProject}(m,H)$ is fully TT for this decoy (via the general ttProject_isTT lemma and nonzero momentum squared of the axis wave).
proof idea
One-line wrapper. The sibling theorem decoy_ttProject_isTT establishes the full IsTT triple for ttProject axisWave decoyLongitudinal. The third conjunct of that triple is exactly IsTransverse. The proof projects with .2.2 and stops.
why it matters
Inside the algebraic edge_tt_decomposition layer (Wave 4 / W4-1), this pins that the TT map really kills a pure longitudinal decoy on the axis wave: the output is transverse, not merely claimed TT by packaging. It sits next to the existence theorem that every symmetric $4\times 4$ matrix decomposes as TT + gauge + transverse-trace residual, and next to the explicit axis TT polarizations used to exhibit two independent polarizations in 4D.
No downstream consumers are wired yet (used_by empty). The module doc is explicit that this layer does not decompose Regge EDGE perturbations, does not prove $S_{\mathrm{RS}}$ converges to Einstein-Hilbert in 4D, and does not flip gap_action_recovery. It is a kernel-checked algebraic checkpoint on the road to those gravity closers, not a continuum or lattice result.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.