decoyTT_isTT
plain-language theorem explainer
The decoy matrix diag(0,0,1,−1) is algebraically transverse-traceless against the axis wave covector (1,0,0,0). Anyone checking nonvacuity of the 4D plane-wave edge TT attachment layer cites this. The proof is a one-line identification with the already-proved plus-polarization TT witness.
Claim. The matrix $\mathrm{diag}(0,0,1,-1)$ is symmetric, Euclidean-traceless, and transverse to the wave covector $m=(1,0,0,0)$ on $\mathbb{R}^4$.
background
This module attaches the Euclidean $4\times 4$ TT / gauge / transverse-trace split to plane-wave edge loadings on axis edges of the 4-torus. It sits one layer above the algebraic decomposition file: same quadratic-form convention as the 3D chain, now on axis displacements.
Algebraic TT means three conditions at once: the matrix is symmetric, its Euclidean trace vanishes, and it is transverse to a fixed wave covector $m$ (row and column contractions with $m$ are zero). The axis wave used here is $m=(1,0,0,0)$. The decoy matrix is exactly the algebraic plus polarization $\mathrm{diag}(0,0,1,-1)$ against that axis wave; the upstream lemma already records that this polarization is TT.
The surrounding section is labeled nonvacuity: the campaign needs at least one concrete nonzero TT edge perturbation before talking about edge loadings and discrete Lie identities for gauge parts.
proof idea
One-line term wrapper. The decoy matrix is definitionally equal to the plus polarization, so the claim reduces to the upstream theorem that the plus polarization is TT against the axis wave. No new case analysis or arithmetic is performed here.
why it matters
Inside the QG Wave-4 lane on edge TT decomposition, this is the concrete nonzero TT witness for the plane-wave attachment layer. The module already proves edge-load linearity, transport of the algebraic TT+gauge+trace split to axis edges, and the exact finite-difference identity linking gauge-part edge load to discrete Lie loading. Without a named nonzero TT matrix, those identities risk looking vacuous on the TT summand.
No downstream consumer is wired yet (used-by is empty). The result does not close the ledger name edge_tt_decomposition in full, does not recover continuum Einstein-Hilbert, and does not flip gap_action_recovery or S_RS_converges_EH_4d. It is a kernel-checked nonvacuity pin in the 4D Regge edge campaign, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.