euclideanTrace_sub
plain-language theorem explainer
Euclidean trace on real 4×4 matrices is linear under subtraction: tr(A−B)=tr(A)−tr(B). Anyone building the algebraic transverse-traceless projector in 4D cites this when peeling residual traces. The proof is a one-line unfold of the diagonal sum plus Finset sum distributivity.
Claim. For any real $4\times 4$ matrices $A$ and $B$, the Euclidean trace satisfies $\mathrm{tr}(A-B)=\mathrm{tr}(A)-\mathrm{tr}(B)$, where $\mathrm{tr}(H):=\sum_{i=0}^{3} H_{ii}$.
background
This module is the algebraic layer of the 4D edge transverse-traceless (TT) decomposition: linear algebra of symmetric real $4\times 4$ matrices against a nonzero Euclidean wave covector on $\mathrm{Fin},4$. It lifts the 3D TT conventions (Euclidean trace, transversality, symmetry) without a Frobenius pin; Minkowski specialization is deferred.
Matrices are Mat4, i.e. $\mathrm{Matrix}(\mathrm{Fin},4)(\mathrm{Fin},4),\mathbb{R}$. The Euclidean trace is the plain diagonal sum $\sum_{i} H_{ii}$. No Lorentzian signature enters here; the object is the same Euclidean trace used in the 3D closer chain.
The result is pure finite-dimensional linear algebra over $\mathbb{R}$. Upstream name collisions on the letter $A$ (active-edge counts elsewhere in the monolith) are unrelated; only the local matrix arguments matter.
proof idea
One-line wrapper. Unfold the definition of Euclidean trace (diagonal sum over $\mathrm{Fin},4$), then apply simp with Finset.sum_sub_distrib, which pushes subtraction through the finite sum entrywise. No matrix algebra beyond componentwise subtraction is required.
why it matters
Feeds two local parents in the same file. First, the trace of the transverse projector equals 3: after unfolding that projector as $I$ minus a scaled outer square, this lemma splits the trace so the identity contributes 4 and the rank-one piece contributes 1. Second, the TT projection is traceless: residual-trace subtraction is rewritten via the same identity plus the projector-trace fact.
In the QG campaign this sits in Wave 4 / lane W4-1 (edge_tt_decomposition), the smallest kernel-checked algebraic increment toward a 4D TT split. It does not itself close continuum Einstein-Hilbert recovery or flip gap-action recovery; it only supplies the trace-linearity step those later algebraic lemmas need. Framework landmarks T7/T8 (eight-tick, $D=3$) are ambient context for why 4D spacetime matrices appear, not inputs to this identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.