lorentzLoad_gaugePart
plain-language theorem explainer
The Lorentz load of a pure gauge piece built from covectors m and v equals (m·m)v + m(v·m) componentwise. Anyone checking that gauge corrections cancel the longitudinal load of a symmetric 4×4 matrix against a Minkowski wave covector cites this identity. The proof is a short Fin-sum calc: distribute, factor constants, and rewrite the two pairings via the sum form of the Minkowski product.
Claim. For covectors $m,v:\mathbb{R}^4$ and any index $i$, the Lorentz load of the symmetrized outer product $m\otimes_s v$ against $m$ satisfies $(\mathrm{load}(m\otimes_s v,m))_i = (m\cdot m)\,v_i + m_i\,(v\cdot m)$, where $\cdot$ is the Minkowski pairing and the load contracts the second index against the raised covector $m^\sharp$.
background
This module is the Lorentzian algebraic layer of the edge TT decomposition campaign (Wave 4 / W4-1): transverse-traceless splitting of symmetric real $4\times 4$ 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 component.
The gauge piece is the symmetrized outer product $(m\otimes_s v)_{ij}=m_i v_j+v_i m_j$. The Lorentz load of a covariant matrix $H$ is $(\mathrm{load}(H,m))i=\sum_j H{ij}(m^\sharp)^j$, i.e. contraction of the second index against the raised wave covector. The Minkowski pairing is $\eta^{ij}a_i b_j$, equivalently $\sum_i a_i(b^\sharp)^i$ by the companion identity minkowskiDot_eq_sum.
The Euclidean sibling module uses the same gauge-part formula; here the metric is Minkowski, so loads and traces use raise and minkowskiDot rather than the Euclidean inner product.
proof idea
Unfold load and gaugePart to the explicit sum $\sum_j(m_i v_j+v_i m_j)(m^\sharp)^j$. Distribute the product by ring congruence on each summand, then split the sum with Finset.sum_add_distrib. Pull the $i$-independent factors $m_i$ and $v_i$ out via Finset.mul_sum. Rewrite each remaining sum as a Minkowski pairing by minkowskiDot_eq_sum (so $\sum_j v_j(m^\sharp)^j=v\cdot m$ and $\sum_j m_j(m^\sharp)^j=m\cdot m$). A final ring step swaps the two terms into the stated order $(m\cdot m)v_i+m_i(v\cdot m)$.
why it matters
In the Lorentzian TT pipeline one subtracts a pure gauge piece so that the residual is transverse (vanishing Lorentz load). This identity evaluates the load of any such gauge piece in closed form, which is the algebraic engine behind the non-null gauge-vector correction.
The sole recorded consumer is lorentzLoad_gaugePart_gaugeVector: with $v$ chosen as the gauge vector built from $H$ and $m$ (when $m\cdot m\neq 0$), the identity specializes to $\mathrm{load}(m\otimes_s v,m)=\mathrm{load}(H,m)$, so subtracting that gauge piece kills the longitudinal load. That step is local linear algebra inside the ledger name edge_tt_decomposition; it does not yet touch Regge edge perturbations, Einstein–Hilbert recovery, or polarization normalizations.
Relative to the broader Recognition gravity stack this is pure Minkowski 4D algebra supporting the Clausius–Einstein bridge imports, not a forcing-chain (T0–T8) or mass-ladder result.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.