euclideanTrace_outerSq
plain-language theorem explainer
The Euclidean trace of the rank-one outer-square matrix built from a covector m equals the squared Euclidean norm of m. Anyone computing traces of gauge or projector pieces in the 4D TT decomposition cites this identity. The proof is pure definitional equality (rfl).
Claim. For every covector $m:\mathbb{R}^4$, the Euclidean trace of the outer-square matrix $(m\otimes m)_{ij}=m_i m_j$ equals $\sum_{i=0}^{3} m_i^2$.
background
This module is the algebraic layer of the QG campaign lane edge_tt_decomposition: linear-algebra transverse-traceless structure for 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 and without Minkowski specialization.
Three local definitions enter. The Euclidean trace of a matrix $H$ is $\sum_i H_{ii}$. The momentum square of a covector $m$ is $\sum_i m_i^2$. The outer square is the rank-one matrix $(m\otimes m)_{ij}=m_i m_j$. The same outer-square construction appears in the Lorentzian sibling module, but here the ambient metric is Euclidean.
proof idea
One-line definitional equality. Expanding the left-hand side gives $\sum_i (m\otimes m)_{ii}=\sum_i m_i m_i$, which is exactly the right-hand side, so rfl closes the goal with no lemmas.
why it matters
Feeds the next identity euclideanTrace_transverseProjector, which shows that the Euclidean transverse projector built from a nonzero $m$ has trace $3$. That projector is the gauge-cleaned piece of the 4D TT decomposition of symmetric matrices, the algebraic kernel of the ledger name edge_tt_decomposition.
The module is deliberately scoped: it does not decompose Regge EDGE perturbations, does not prove continuum Einstein-Hilbert recovery, and does not flip gap_action_recovery. Within those bounds this trace identity is the elementary step that turns the outer-square gauge term into a scalar momentum factor when traces are taken.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.