decoyLongitudinal
plain-language theorem explainer
Explicit pure-gauge longitudinal decoy on Fin 4: the gauge matrix built from the axis wave covector m=(1,0,0,0) and the unit covector e0. Gravity analysts cite it when checking that TT projection removes non-transverse contamination. Body is a one-line call to the gauge-part constructor.
Claim. Let $m=(1,0,0,0)$ be the axis Euclidean wave covector on $\mathbb{R}^4$, and let $v=e_0=(1,0,0,0)$. The longitudinal decoy is the $4\times 4$ matrix $H_{ij}=m_i v_j+v_i m_j$ (the pure gauge mode along the wave direction).
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 closer (Euclidean trace, Euclidean transversality, symmetry) with no Frobenius pin; Minkowski/null specialization is deferred.
A matrix $H$ is algebraically TT against $m$ when it is symmetric, Euclidean-traceless, and transverse ($\sum_j H_{ij}m_j=0$). The gauge piece is the symmetric rank-at-most-two form $(m\otimes v+v\otimes m)_{ij}=m_i v_j+v_i m_j$. The axis wave is the fixed covector $m=(1,0,0,0)$ used for the explicit two-polarization basis and for decoy tests.
Upstream, exists_edgeTTDecomposition states every symmetric $H$ splits as TT projection plus gauge part plus residual transverse-trace term whenever $m\neq 0$.
proof idea
Definition, not a proof. Instantiates the gauge-part constructor on the axis wave covector with the pure longitudinal vector $v=e_0$ (the indicator of index 0). No lemmas are applied; the matrix entries are exactly $m_i v_j+v_i m_j$.
why it matters
Supplies the concrete non-TT longitudinal sample that the algebraic TT pipeline must reject and then clean. Downstream theorems use it to prove: the decoy is symmetric; it fails transversality against the axis wave; its TT projection is TT (hence transversality is restored); and, in the closer module, the named decoy gauge matrix equals this longitudinal decoy.
That closes a kernel-checked sanity path inside Wave 4 / lane W4-1 without touching Regge edge perturbations, $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$, or gap_action_recovery. It is the 4D analogue of a pure longitudinal contamination used to witness that the projector really kills gauge modes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.