load_outerSq
plain-language theorem explainer
Applying the rank-one outer product m⊗m to the covector m recovers |m|² m componentwise on Fin 4. Anyone building the Euclidean transverse projector or the 4D TT decomposition cites this identity. The proof is a short calc: factor m_i out of the sum, then commute scalars.
Claim. For any covector $m:\mathrm{Fin}\,4\to\mathbb{R}$ and any index $i$, the matrix-vector product of the outer square $(m\otimes m)_{ij}=m_i m_j$ against $m$ satisfies $\sum_j (m_i m_j)m_j = \bigl(\sum_j m_j^2\bigr) m_i$.
background
This module is the algebraic layer of the QG campaign item edge_tt_decomposition: Euclidean transverse-traceless decomposition of symmetric real $4\times 4$ matrices against a nonzero wave covector on $\mathrm{Fin},4$. Conventions lift the 3D closer (Euclidean trace, Euclidean transversality, symmetry) without a Frobenius pin; Lorentzian/null specialization is deferred.
Three local definitions enter the statement. The outer square is the rank-one matrix $(m\otimes m)_{ij}=m_i m_j$. The squared momentum is the Euclidean norm squared $|m|^2=\sum_i m_i^2$. Load is the ordinary matrix-vector product $(\mathrm{load},H,m)i=\sum_j H{ij}m_j$. The claim is the elementary eigenvector identity $(m\otimes m)m=|m|^2 m$.
proof idea
Unfold the three definitions so the goal is $\sum_j(m_i m_j)m_j=(\sum_j m_j^2)m_i$. The first calc step factors $m_i$ out of the finite sum via mul_assoc and Finset.mul_sum. The second step reorders the remaining scalar product by ring. No external lemmas beyond associativity and sum-factorization are required.
why it matters
The identity is the key algebraic step in load_transverseProjector, which proves that the Euclidean transverse projector $I-|m|^{-2}(m\otimes m)$ annihilates $m$ whenever $|m|^2\neq 0$. That projector is the building block of the 4D IsTT / transverse-traceless decomposition on the algebraic layer. The module explicitly does not yet decompose Regge EDGE perturbations, prove $S_{\mathrm{RS}}$ converges to Einstein-Hilbert in 4D, or flip gap_action_recovery; this lemma only closes the linear-algebra kernel needed before those continuum claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.