outerSq_symmetric
plain-language theorem explainer
The rank-one outer-square matrix built from any real 4-vector is symmetric. Algebraic TT-decomposition work on Euclidean 4×4 matrices against a wave covector cites this as a basic structural fact. The proof is a one-line intro-unfold-ring wrapper using commutativity of real multiplication.
Claim. For every real 4-vector $m$, the matrix $H$ with entries $H_{ij} = m_i m_j$ is symmetric: $H_{ij} = H_{ji}$ for all $i,j \in \{0,1,2,3\}$.
background
This module is the algebraic layer of the QG campaign lane edge_tt_decomposition: linear-algebra transverse-traceless decomposition of symmetric real $4\times 4$ 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; Minkowski/null specialization is deferred.
A matrix $H:\mathrm{Fin},4\to\mathrm{Fin},4\to\mathbb{R}$ is symmetric when $H_{ij}=H_{ji}$ for all indices. The outer-square of a covector $m$ is the rank-one matrix $(outerSq,m)_{ij}=m_i m_j$. That object appears inside the transverse projector (identity minus a scaled outer-square of the wave covector), so symmetry of the outer-square is the first structural lemma needed before projector symmetry and the TT predicates.
proof idea
One-line wrapper. Introduce indices $i,j$, unfold the outer-square definition to $m_i m_j$, and close by ring, which uses commutativity of multiplication in $\mathbb{R}$ to obtain $m_i m_j = m_j m_i$. No external lemmas are required.
why it matters
Feeds transverseProjector_symmetric in the same module: that proof unfolds the projector and rewrites the outer-square legs via this lemma. The Lorentzian twin module copies the same statement and uses it analogously (together with Minkowski-eta symmetry) for its own transverse projector. Within the Recognition gravity stack this is pure linear-algebra scaffolding for the edge TT decomposition; it does not itself close continuum or lattice recovery goals, but without it the projector cannot be shown symmetric and the TT conjuncts cannot start.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.