euclideanTrace_transverseProjector
plain-language theorem explainer
For any nonzero Euclidean covector m on R^4, the transverse projector P_m = I - m⊗m/|m|^2 has Euclidean trace equal to 3. Gravity analysts cite this when checking that the algebraic TT projection is traceless. The proof unfolds the projector and reduces via linearity of the diagonal sum to the identity 4 - 1 = 3.
Claim. Let $m \in \mathbb{R}^4$ satisfy $|m|^2 := \sum_{i=0}^{3} m_i^2 \neq 0$. Write $P_m$ for the Euclidean transverse projector $I - (m \otimes m)/|m|^2$ on $4 \times 4$ real matrices. Then the Euclidean trace $\mathrm{tr}_E(P_m) := \sum_i (P_m)_{ii}$ equals $3$.
background
This module is the algebraic layer of the QG campaign item edge_tt_decomposition: linear-algebra TT structure for symmetric $4 \times 4$ real 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; Lorentzian/null specialization is deferred.
The Euclidean trace is the plain diagonal sum $\mathrm{tr}E(H) = \sum{i:F\mathrm{in},4} H_{ii}$. The squared momentum is $|m|^2 = \sum_i m_i^2$. The outer-square matrix has entries $m_i m_j$, and the transverse projector is the rank-3 endomorphism $I - |m|^{-2},(m \otimes m)$ orthogonal to $m$.
Upstream facts used here: $\mathrm{tr}_E(I)=4$, $\mathrm{tr}_E(m\otimes m)=|m|^2$, and linearity of $\mathrm{tr}_E$ under scalar multiplication and subtraction.
proof idea
Term-mode proof by unfolding the projector definition, then rewriting with the four trace lemmas: trace of a difference, trace of a scalar multiple, $\mathrm{tr}_E(I)=4$, and $\mathrm{tr}_E(m\otimes m)=|m|^2$. After those rewrites one has $4 - |m|^{-2}\cdot|m|^2$. field_simp discharges the nonzero denominator hypothesis and ring closes $4-1=3$.
why it matters
The immediate consumer is ttProject_traceless: the residual-trace correction in the algebraic TT projector is scaled by $\mathrm{tr}_E(P_m)$, so knowing that factor equals 3 makes the projected matrix Euclidean-traceless. That is one of the three conjuncts in the local IsTT predicate (symmetric, traceless, transverse) that the 4D edge TT decomposition must deliver.
In the campaign framing this is pure linear algebra on the Euclidean side of Wave 4 / lane W4-1. It does not yet touch continuum Lorentz polarizations, Regge edge modes, or the action-recovery gap; it only locks the trace dimension of the transverse screen so downstream TT identities stay kernel-checked.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.