IsTT
plain-language theorem explainer
Algebraic transverse-traceless (TT) predicate on a real 4×4 matrix relative to a Euclidean wave covector: the matrix is symmetric, Euclidean-traceless, and annihilates the covector on each row. Gravity and continuum second-variation proofs cite it as the hypothesis that collapses linearized Ricci and Einstein operators to pure wave terms. The body is a three-way conjunction of the local symmetry, trace, and transversality predicates.
Claim. A real $4\times 4$ matrix $H$ is algebraically transverse-traceless with respect to a covector $m\in\mathbb{R}^4$ when $H$ is symmetric ($H_{ij}=H_{ji}$), Euclidean-traceless ($\mathrm{tr}_E H=0$), and transverse to $m$ ($\sum_j H_{ij}m_j=0$ for every row index $i$).
background
This module is the algebraic layer of the QG campaign lane edge_tt_decomposition: the linear-algebra TT decomposition of symmetric real $4\times 4$ matrices against a nonzero Euclidean wave covector on $\mathrm{Fin},4$. It deliberately stays Euclidean (trace and transversality), with Minkowski/null specialization deferred.
Mat4 is the abbreviation for real $4\times 4$ matrices. The three conjuncts are local: symmetry means $H_{ij}=H_{ji}$; tracelessness means the Euclidean trace vanishes; transversality means each row of $H$ is orthogonal to the covector $m$. The same three conditions appear in the 3D closer chain (IsTTPolarization); this file lifts them to four indices without a Frobenius pin.
Upstream cost-algebra and d'Alembert symmetry names collide only as identifiers; the matrix predicates used here are the in-module geometric ones, not the functional $F(x)=F(1/x)$ symmetry of the Recognition cost.
proof idea
Pure definition: the predicate is the conjunction of the three in-module props IsSymmetric, IsTraceless, and IsTransverse. No tactics, no lemmas, no computation.
why it matters
This is the gate hypothesis for the continuum TT second-variation stack. Downstream theorems such as linRicci_tt (linearized Ricci equals $\tfrac12$ times momentum-squared times the wave amplitude on TT data), linRicciScalar_tt (scalar vanishes), linEinstein_tt, and ehSecondVariationDensity_tt all take an IsTT hypothesis and reduce curvature operators to pure massless-wave expressions. Higher faces (density_factors_through_phase, ehFace_eq_average_of_density) inherit the same gate, so the Einstein-Hilbert face average is well-defined only on this algebraic TT locus.
In the Recognition gravity program this is the algebraic kernel of Wave 4 / W4-1. It does not itself close Regge edge perturbations, $S_{RS}\to EH$ convergence, or gap_action_recovery; those remain separate ledger items. The definition simply names the three Euclidean conditions that later continuum identities need.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.