load_gaugePart
plain-language theorem explainer
The matrix-vector load of a pure gauge symmetric 4×4 block against the wave covector m equals |m|² times the gauge vector plus a longitudinal term m_i(v·m). Algebraic-layer users of the 4D edge TT decomposition cite this when stripping gauge from a symmetric matrix. The proof is a short calc: expand the bilinear gauge form, distribute the sum, and rearrange by ring.
Claim. Let $m,v\in\mathbb{R}^4$ and fix an index $i$. Write $G_{ij}=m_i v_j+v_i m_j$ for the symmetric gauge matrix built from $m$ and $v$. Then $\sum_j G_{ij}m_j=|m|^2\,v_i+m_i(v\cdot m)$, where $|m|^2=\sum_k m_k^2$ and $v\cdot m=\sum_k v_k m_k$.
background
This module is the algebraic layer of the QG campaign item edge_tt_decomposition: linear-algebra transverse-traceless splitting of symmetric real 4×4 matrices against a nonzero Euclidean wave covector on Fin 4. It lifts the 3D IsTTPolarization conventions (Euclidean trace, Euclidean transversality, symmetry) without a Frobenius pin; Lorentzian/null specialization is deferred.
The gauge matrix is the symmetric outer form $G_{ij}=m_i v_j+v_i m_j$. Load is the Euclidean matrix-vector product $(\mathrm{load},H,m)i=\sum_j H{ij}m_j$. Momentum-squared is the squared Euclidean norm of $m$, and the local dot is the ordinary Euclidean pairing on $\mathbb{R}^4$ (the Cost.Ndim weighted dot is the same shape on general Fin n).
Together these give the elementary identity that load of a pure gauge block is a linear combination of $v$ and $m$, which is the algebraic engine for later gauge subtraction.
proof idea
Unfold load, gaugePart, momentumSq, and dot. The left-hand side is $\sum_j(m_i v_j+v_i m_j)m_j$. A Finset.sum_congr with ring rewrites each summand as $m_i(v_j m_j)+v_i(m_j m_j)$. Split by Finset.sum_add_distrib, pull constants with Finset.mul_sum, then ring to reorder as $|m|^2 v_i+m_i(v\cdot m)$. No external lemmas beyond Mathlib sum algebra.
why it matters
Parent use is load_gaugePart_gaugeVector, which shows that loading the gauge part built from the canonical gauge vector recovers the full load of H: after setting $v$ to that gauge vector, this identity cancels the residual and proves load(gaugePart m v)m = load H m componentwise (when $|m|^2\neq 0$).
In the Recognition gravity stack this is pure linear algebra supporting the TT projector on edges: gauge modes must drop out of the transverse-traceless sector before any continuum or Regge comparison. The module doc is explicit that this file does not yet decompose Regge EDGE perturbations, does not prove S_RS_converges_EH_4d, and does not flip gap_action_recovery. It is the smallest kernel-checked increment on lane W4-1 toward those closers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.