IsTraceless
plain-language theorem explainer
A real 4×4 matrix is Euclidean-traceless when the sum of its diagonal entries vanishes. Gravity and continuum-TT analyses cite this predicate as one of the three conjuncts of algebraic TT (with symmetry and transversality). The body is a one-line definitional equality to the Euclidean trace.
Claim. A matrix $H \in M_4(\mathbb{R})$ is Euclidean-traceless when $\sum_{i=0}^{3} H_{ii} = 0$.
background
This module is the algebraic layer of the 4D edge transverse-traceless decomposition: linear algebra of symmetric $4\times 4$ real matrices against a nonzero Euclidean wave covector on $\mathrm{Fin},4$. It lifts the 3D TT conventions (Euclidean trace, Euclidean transversality, symmetry) without a Frobenius pin; Minkowski/null specialization is deferred.
Mat4 is the abbreviation for $M_4(\mathbb{R})$. The Euclidean trace is the plain diagonal sum $\sum_{i} H_{ii}$, not a Lorentzian contraction. Tracelessness here is that scalar condition set to zero.
Upstream cost-algebra symbols named $H$ appear only as name collisions with the matrix parameter; the mathematical content of this predicate depends only on the Euclidean trace of a $4\times 4$ matrix.
proof idea
Definitional: the predicate is exactly the proposition that the Euclidean trace equals zero. No lemmas or tactics.
why it matters
Algebraic TT is the conjunction of symmetry, this tracelessness predicate, and transversality to the wave covector. Downstream, the axis plus and cross polarizations discharge the traceless conjunct by direct evaluation of the four-term diagonal sum; the TT projector is proved traceless for any nonzero momentum squared. Continuum second-variation work uses the hypothesis to kill the summed Christoffel-amplitude diagonal. In the QG campaign this is kernel infrastructure for edge_tt_decomposition (Wave 4 / W4-1), not yet a lattice Regge edge decomposition or an Einstein-Hilbert convergence statement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.