minkowskiTrace_outerSq
plain-language theorem explainer
The Minkowski metric-trace of the rank-one outer product $m_i m_j$ equals the Minkowski square of the covector $m$. Anyone assembling Lorentzian transverse projectors or TT gauges cites this identity. The proof is a one-line unfold of the three definitions followed by ring.
Claim. For every covector $m \in \mathbb{R}^4$, if $(m \otimes m)_{ij} := m_i m_j$, then $\eta^{ij}(m \otimes m)_{ij} = m \cdot_\eta m$, i.e. $-(m_0)^2 + m_1^2 + m_2^2 + m_3^2$.
background
This module is the Lorentzian algebraic layer of the edge TT decomposition campaign (Wave 4 / W4-1): transverse-traceless splitting of symmetric $4\times 4$ real matrices against a Minkowski wave covector on $\mathrm{Fin},4$, including the null case. Signature is $(-,+,+,+)$; covectors are lowered by default.
The Minkowski pairing of covectors is $\mathrm{minkowskiDot}(a,b)=-(a_0)(b_0)+\sum_{k=1}^3 a_k b_k$, equal to $\eta^{ij}a_i b_j$. The metric-trace of a covariant matrix is $\mathrm{minkowskiTrace}(H)=-(H_{00})+H_{11}+H_{22}+H_{33}$. The outer-square map sends $m$ to the rank-one matrix $(m\otimes m)_{ij}=m_i m_j$ (same definition as in the Euclidean sibling module).
These three definitions are the only inputs. No projector or transversality hypothesis appears yet; the identity is pure linear algebra on the Minkowski metric.
proof idea
One-line wrapper: unfold the three definitions (metric-trace, outer-square, Minkowski pairing) and finish with ring. Expanding gives $-(m_0 m_0)+m_1 m_1+m_2 m_2+m_3 m_3$ on the left, which is exactly the pairing of $m$ with itself.
why it matters
Feeds the non-null projector trace identity: $\mathrm{minkowskiTrace}(\mathrm{transverseProjector},m)=3$ when $m\cdot m\neq 0$. That rewrite chain subtracts a scaled outer-square from $\eta$, so it needs this lemma to replace the outer-square contribution by $m\cdot m$ and cancel. Without it the projector rank (trace 3) is not kernel-checked.
In the broader RS gravity stack this sits in the Lorentzian linear-algebra layer of the ledger name edge_tt_decomposition. It does not itself decompose Regge edge modes or recover the Einstein-Hilbert action; it only supplies the algebraic bookkeeping those later steps require when building TT gauges against a wave covector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.