load_transverseProjector
plain-language theorem explainer
The Euclidean transverse projector built from a nonzero covector m on Fin 4 is itself transverse: its load against m is the zero covector. Anyone showing that the TT projection lands in the transverse subspace cites this identity. The proof unfolds the projector as I minus the normalized outer square and cancels componentwise via the load lemmas for identity, scalar multiple, outer square, and subtraction.
Claim. Let $m \in \mathbb{R}^{4}$ satisfy $|m|^{2} \neq 0$, and write $P(m) = I - \frac{m m^{\top}}{|m|^{2}}$ for the Euclidean transverse projector. Then for every index $i$, the load of $P(m)$ against $m$ vanishes: $\bigl(P(m)\, m\bigr)_{i} = 0$.
background
This module is the algebraic layer of the edge TT decomposition campaign (Wave 4 / W4-1): linear-algebra transverse-traceless decomposition of symmetric real $4\times 4$ matrices against a nonzero Euclidean wave covector on $\mathrm{Fin},4$. Conventions lift the 3D closer chain (Euclidean trace, Euclidean transversality, symmetry) with no Frobenius pin; Minkowski specialization is deferred.
The load of a matrix $H$ against a covector $m$ is the ordinary matrix-vector product $(\mathrm{load}, H, m){i} = \sum{j} H_{ij} m_{j}$. The squared momentum is $|m|^{2} = \sum_{i} m_{i}^{2}$. The outer-square matrix has entries $m_{i} m_{j}$. The transverse projector is the standard rank-one update $P(m) = I - |m|^{-2}, m m^{\top}$.
Upstream load lemmas already record how load interacts with the identity ($\mathrm{load}, I, m = m$), scalar multiples, subtraction, and the outer square ($\mathrm{load},(mm^{\top}), m = |m|^{2}, m$).
proof idea
Unfold the definition of the transverse projector. Rewrite the load of the resulting difference using the four algebraic load lemmas: load of a difference splits, load of the identity returns $m_{i}$, load of a scalar multiple factors the coefficient, and load of the outer square returns $|m|^{2}, m_{i}$. After those rewrites the goal is the elementary identity $m_{i} - |m|^{-2}\cdot(|m|^{2}, m_{i}) = 0$. Discharge the nonzero denominator with field_simp on the hypothesis $|m|^{2}\neq 0$, then finish by ring.
why it matters
Transversality of the projector is the first half of showing that the TT projection operator lands in the transverse-traceless subspace. The immediate parent is ttProject_transverse, which reduces componentwise transversality of the projected matrix to a load-vanishing statement and invokes this lemma on the gauge-corrected piece.
In the Recognition Science gravity lane this sits inside the algebraic kernel of edge_tt_decomposition: it is the 4D lift of the Euclidean transversality conjunct used by the 3D IsTTPolarization closer. It does not yet touch continuum Lorentzian polarizations, Regge edge perturbations, or the action-recovery gap; those remain separate campaign items. The result is fully proved (no sorry, no extra axioms beyond the expected classical footprint).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.