lorentzLoad_outerSq
plain-language theorem explainer
The Lorentz load of the rank-one outer product m⊗m against the wave covector m equals the Minkowski self-pairing of m times the component m_i. Builders of the non-null Lorentz transverse projector and null-axis counterexamples cite this contraction identity. The proof factors m_i from the sum and rewrites the residual contraction via the sum form of the Minkowski pairing.
Claim. For any covector $m\in\mathbb{R}^4$ and index $i\in\{0,1,2,3\}$, if $H_{jk}=m_j m_k$ is the outer-product matrix of $m$, then the Lorentz load $(H\cdot m^\sharp)_i$ equals $(m\cdot m)\,m_i$, where $m\cdot m$ is the Minkowski pairing of covectors and $m^\sharp$ is $m$ with its time component sign-flipped.
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; index raising negates the time slot, $(m^\sharp)_0=-m_0$ and $(m^\sharp)_i=m_i$ spatially.
The Minkowski pairing is $m\cdot m=-(m_0)^2+\sum_{k=1}^3(m_k)^2$, equivalently $\sum_j m_j(m^\sharp)_j$ by the upstream identity minkowskiDot_eq_sum. The Lorentz load of a matrix $H$ is the covector $(H\cdot m^\sharp)i=\sum_j H{ij}(m^\sharp)j$. The outer-square matrix is the rank-one product $H{ij}=m_i m_j$, carried over from the Euclidean sibling module.
Lorentz transversality is exactly vanishing of this load. The non-null transverse projector subtracts a multiple of the outer square from $\eta$, so the load of that outer square must be known explicitly.
proof idea
Unfold the load and the outer square to obtain $\sum_j(m_i m_j)(m^\sharp)_j$. Factor $m_i$ out of the finite sum with associativity and Finset.mul_sum, leaving $m_i\sum_j m_j(m^\sharp)_j$. Rewrite the residual sum as the Minkowski self-pairing via minkowskiDot_eq_sum, then commute the real product by ring. Pure algebraic one-calc proof; no case split on null or non-null.
why it matters
This is the contraction identity that makes the non-null Lorentz transverse projector actually transverse. Downstream, lorentzLoad_transverseProjector applies it after subtracting the scaled outer square from $\eta$, then cancels with field_simp under $m\cdot m\neq 0$. The same identity feeds the null-axis counterexample euclideanProjector_not_lorentzTransverse_on_nullAxis, which shows the Euclidean projector (well-defined because the Euclidean norm is $2$) fails Lorentz transversality on a null wave covector.
In the QG ledger this sits inside the algebraic half of edge_tt_decomposition: it does not yet touch Regge edge perturbations, $S_{\mathrm{RS}}\to EH$, or gap-action recovery, but it closes the linear-algebra step needed before those geometric claims. Framework-wise it is pure Minkowski linear algebra supporting the gravity analysis lane, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.