decoyLongitudinal_not_transverse
plain-language theorem explainer
A pure gauge (longitudinal) 4×4 mode built from the axis wave covector fails Euclidean transversality. Anyone checking that the algebraic TT summand is the only transverse piece in the 4D edge decomposition cites this. The proof is a one-step specialization: assume transversality, evaluate the i=0 row sum, and simplify to 2=0.
Claim. Let $m=(1,0,0,0)$ be the axis wave covector on $\mathbb{R}^4$, and let $H$ be the pure gauge matrix $H_{ij}=m_i v_j+v_i m_j$ for the longitudinal vector $v=(1,0,0,0)$. Then $H$ is not transverse to $m$: it is false that $\sum_j H_{ij}m_j=0$ for every row $i$.
background
This module is the algebraic layer of the QG ledger 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 conventions (Euclidean trace, Euclidean transversality, symmetry) without a Frobenius pin; Minkowski/null specialization is deferred.
Transversality means every row of $H$ is orthogonal to the wave covector $m$: $\sum_j H_{ij}m_j=0$. The gauge piece is the symmetric outer form $\mathrm{gaugePart}(m,v)_{ij}=m_i v_j+v_i m_j$. The decoy longitudinal matrix is exactly that gauge piece for $m=\mathrm{axisWave}=(1,0,0,0)$ and $v=(1,0,0,0)$, so it is a pure longitudinal contamination one must exclude from the TT summand.
The ambient existence theorem states every symmetric $H$ splits as TT plus gauge plus residual transverse-trace against any $m$ with nonzero Euclidean momentum squared.
proof idea
Term-mode by contradiction. Assume transversality of the decoy. Specialize the universal quantifier to row $i=0$. Unfold the decoy as gaugePart of axisWave against the indicator vector on coordinate 0, expand the four-term Fin sum, and simplify: the only surviving contribution is $2$, so $2=0$.
why it matters
Closes a negative control in the algebraic TT story: pure gauge modes are not transverse, so they cannot hide inside the TT projector. Downstream, decoyGauge_not_transverse rewrites its decoy to this longitudinal matrix and applies the present theorem verbatim, feeding the named ledger closer on the algebraic-plus-attachment layer.
In the broader campaign this sits under Wave 4 / lane W4-1. It does not itself recover Einstein–Hilbert continuum limits or flip gap-action recovery; it only certifies that the longitudinal decoy is correctly excluded from the transverse-traceless cone used when counting two independent 4D polarizations on the axis wave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.