outerSq
plain-language theorem explainer
Sends a real 4-vector m to the rank-at-most-one matrix with entries m_i m_j (the Euclidean outer product). Cited by anyone building the transverse projector, load map, or trace identities in the 4D edge TT algebraic layer. Body is the pointwise product; no proof content.
Claim. For $m \in \mathbb{R}^4$, the outer-square matrix is the $4\times 4$ real matrix with entries $(m \otimes m)_{ij} = m_i m_j$.
background
Module is the algebraic layer of the QG full-theory campaign lane W4-1 (edge_tt_decomposition): linear-algebra TT decomposition of symmetric real $4\times 4$ matrices against a nonzero Euclidean wave covector on $\mathrm{Fin},4$. Conventions lift the 3D package (Euclidean trace, Euclidean transversality, symmetry) with no Frobenius pin; Minkowski/null work is deferred.
Mat4 is simply $\mathrm{Matrix}(\mathrm{Fin},4)(\mathrm{Fin},4),\mathbb{R}$. The outer square is the elementary rank-one block used to form the transverse projector $I - (m\cdot m)^{-1}(m\otimes m)$ and to state load and trace identities relative to the wave covector. An identical entrywise definition lives in the Lorentzian sibling module.
proof idea
Definition only: the matrix is the pointwise product $(i,j)\mapsto m_i m_j$. No lemmas, no tactics, no proof obligations beyond typechecking against Mat4.
why it matters
Kernel building block for the Euclidean TT package. Downstream: outerSq_symmetric (symmetry by commutativity of $\mathbb{R}$), euclideanTrace_outerSq (trace equals momentum squared), load_outerSq (load recovers $|m|^2 m$), and transverseProjector itself. Cross-module uses include the Lorentzian euclideanTransverseProjector, lorentzLoad_outerSq, and minkowskiTrace_outerSq. Supplies the rank-one piece against which the algebraic TT decomposition is written. Does not close Regge EDGE perturbations, S_RS_converges_EH_4d, or gap_action_recovery; those remain outside this algebraic increment.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.