minkowskiTrace_transverseProjector
plain-language theorem explainer
The Minkowski metric-trace of the non-null transverse projector built from a covector m is exactly 3. Anyone assembling Lorentz TT projections of symmetric 4×4 matrices cites this identity. The proof unfolds the projector, applies linearity and the known traces of η and of the outer square, then cancels by field simplification and ring.
Claim. Let $m\in\mathbb{R}^4$ satisfy $m\cdot m\neq 0$ under the Minkowski pairing of signature $(-+++)$. The transverse projector $P_{ij}=\eta_{ij}-m_i m_j/(m\cdot m)$ has Minkowski metric-trace $\eta^{ij}P_{ij}=3$.
background
This module is the Lorentzian algebraic layer of the edge TT decomposition campaign (Wave 4 / W4-1): transverse-traceless splitting of symmetric real $4\times 4$ matrices against a Minkowski wave covector on $\mathrm{Fin},4$, including the null case. Signature is $(-+++)$; covectors are lowered by default; index raising flips the sign of the time component.
The Minkowski pairing is $\mathrm{minkowskiDot}(a,b)=-(a_0)(b_0)+\sum_{i=1}^3 a_i b_i$. The metric-trace of a covariant matrix is $\mathrm{minkowskiTrace}(H)=-(H_{00})+H_{11}+H_{22}+H_{33}$, i.e. $\eta^{ij}H_{ij}$. For non-null $m$ the transverse projector is $P=\eta-(m\cdot m)^{-1},m\otimes m$ (outer square).
Upstream facts used here: $\mathrm{minkowskiTrace}(\eta)=4$, $\mathrm{minkowskiTrace}(m\otimes m)=m\cdot m$, and homogeneity/additivity of the metric-trace under scalar multiplication and subtraction.
proof idea
Term-mode proof by direct expansion. Unfold the non-null transverse projector to $\eta-c\cdot(m\otimes m)$ with $c=(m\cdot m)^{-1}$. Rewrite the metric-trace through the subtraction and scalar-multiplication lemmas, then insert $\mathrm{minkowskiTrace}(\eta)=4$ and $\mathrm{minkowskiTrace}(m\otimes m)=m\cdot m$. The hypothesis $m\cdot m\neq 0$ lets field_simp clear the denominator; ring finishes $4-1=3$.
why it matters
Feeds the single downstream consumer ttProject_traceless, which shows that the Lorentz TT projection of any symmetric matrix is metric-traceless: the residual-trace subtraction uses exactly this identity that $\mathrm{tr}\eta(P)=3$. In the QG full-theory campaign this is pure linear algebra for the ledger name edge_tt_decomposition; it does not yet touch Regge edge perturbations, $S{\mathrm{RS}}\to\mathrm{EH}_{4d}$, or gap-action recovery. Within Recognition Science gravity it supplies the algebraic count of spatial degrees of freedom (trace 3 rather than 4) once the time direction is projected out by a non-null wave covector, consistent with the $D=3$ spatial landmark of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.