transverseProjector
plain-language theorem explainer
Defines the Euclidean transverse projector on 4×4 matrices for a wave covector m: the identity minus the normalized outer product of m. Gravity analysts cite it when building the algebraic TT decomposition of symmetric matrices against a nonzero Euclidean momentum. The body is a one-line matrix expression in terms of momentum-squared and the outer-square map.
Claim. For a covector $m \in \mathbb{R}^4$, the transverse projector is the $4\times 4$ matrix $P(m) = I - \frac{1}{\|m\|_2^2}\, m\otimes m$, where $\|m\|_2^2 = \sum_{i=0}^{3} m_i^2$ and $(m\otimes m)_{ij} = m_i m_j$.
background
This module is the algebraic layer of the QG campaign item edge_tt_decomposition: linear-algebra TT splitting of symmetric real $4\times 4$ matrices against a nonzero Euclidean wave covector on $\mathrm{Fin},4$. Conventions match the 3D TT polarization chain (Euclidean trace, Euclidean transversality, symmetry); Minkowski specialization is deferred to the Lorentz sibling.
Mat4 is an abbreviation for real $4\times 4$ matrices. The squared Euclidean momentum is $\mathrm{momentumSq}(m)=\sum_i m_i^2$, and $\mathrm{outerSq}(m)$ is the rank-one matrix $(m\otimes m)_{ij}=m_i m_j$. The projector subtracts that outer product, scaled by the reciprocal of the squared norm, from the identity.
The Lorentz twin replaces the Euclidean identity and norm by Minkowski $\eta$ and $\eta(m,m)$; the Euclidean form here is the kernel used by the edge decomposition theorems in this file.
proof idea
Pure definition: expand as the matrix difference $I - (\mathrm{momentumSq}, m)^{-1}\bullet\mathrm{outerSq}, m$. No tactics or lemmas; downstream identities unfold this expression and rewrite with trace, load, and symmetry lemmas for the identity and outer-square pieces.
why it matters
This projector is the geometric kernel of the algebraic edge TT decomposition. It appears in ttProject (subtract residual transverse-trace part), in load_transverseProjector (proves $P(m)m=0$), in transverseProjector_symmetric and euclideanTrace_transverseProjector (trace equals 3 when $m\neq 0$), and in the existence theorems exists_edgeTTDecomposition / exists_edgeTTDecomposition' that write every symmetric $H$ as TT plus gauge plus a multiple of $P(m)$.
Those existence results are the named THEOREM layer for ledger item edge_tt_decomposition. The module doc is explicit that this does not yet decompose Regge EDGE perturbations, prove $S_{\mathrm{RS}}$ converges to Einstein–Hilbert in 4D, or flip gap_action_recovery. The Lorentz file reuses the same pattern with Minkowski data for continuum TT counts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.