outerSq_symmetric
plain-language theorem explainer
The rank-one outer-square matrix built from any real covector on Fin 4 is symmetric. Gravity analysts assembling the Lorentzian transverse projector (null or non-null) cite this elementary fact. The proof is a one-line unfold of the product definition followed by ring commutativity.
Claim. For every covector $m:\mathbb{R}^{4}$, the matrix $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 Lorentzian algebraic layer of the QG campaign lane edge_tt_decomposition: transverse-traceless decomposition of symmetric $4\times 4$ real matrices against a Minkowski wave covector, including the null case. Signature is $(-,+,+,+)$; covectors are lowered by default.
Mat4 is the type of maps Fin 4 → Fin 4 → ℝ. Symmetry of such a matrix means $H_{ij}=H_{ji}$ for all index pairs. The outer-square construction is the rank-one matrix $(outerSq,m){ij}=m{i}m_{j}$, identical in form to the Euclidean sibling in EdgeTTDecomposition4D.
The same outer-square appears inside both the non-null projector $P_{ij}=\eta_{ij}-m_{i}m_{j}/(m\cdot m)$ and the null projector that mixes $m$ with an auxiliary null covector $l$.
proof idea
One-line wrapper. Introduce indices $i,j$, unfold the definition of the outer-square matrix to the product $m_{i}m_{j}$, and finish by ring, which uses commutativity of real multiplication to obtain $m_{i}m_{j}=m_{j}m_{i}$. No external lemmas are required.
why it matters
Feeds the local transverseProjector_symmetric theorem, which rewrites the projector difference using this fact together with Minkowski-metric symmetry. The Euclidean twin in EdgeTTDecomposition4D is the same statement and is likewise used by that module's projector symmetry lemma.
Inside the Recognition Science gravity stack this is pure linear-algebra scaffolding for the Lorentzian TT layer of edge_tt_decomposition (Wave 4 / W4-1). It does not itself touch the forcing chain T0–T8, the Recognition Composition Law, or the Einstein–Hilbert recovery goals; those sit further downstream once the algebraic projector is in place.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.