gaugePart
plain-language theorem explainer
Defines the pure-gauge piece of a 4×4 symmetric matrix relative to a Euclidean wave covector m and a gauge vector v: the outer-sum matrix with entries m_i v_j + v_i m_j. Anyone citing the algebraic edge TT decomposition uses this as the longitudinal correction term. The body is a one-line pointwise formula, identical to the Lorentzian twin.
Claim. For covectors $m,v:\mathbb{R}^4\to\mathbb{R}$, the gauge part is the $4\times 4$ real matrix $(G(m,v))_{ij}=m_i v_j+v_i m_j$.
background
This module is the algebraic layer of the QG campaign item edge_tt_decomposition: linear-algebra transverse-traceless splitting of symmetric real $4\times 4$ matrices against a nonzero Euclidean wave covector on $\mathrm{Fin},4$. Conventions lift the 3D closer (Euclidean trace, Euclidean transversality, symmetry) with no Frobenius pin; Minkowski specialization is deferred.
Mat4 is simply $\mathrm{Matrix}(\mathrm{Fin},4,\mathrm{Fin},4,\mathbb{R})$. The gauge part is the standard symmetric outer-sum that generates pure-gauge (longitudinal) deformations of a metric perturbation along $m$. The same formula appears upstream in the Lorentzian 4D twin module; this Euclidean copy is the one consumed by the existence theorems in the present file.
proof idea
Definitional one-liner: the matrix is declared by the pointwise rule $(i,j)\mapsto m_i v_j+v_i m_j$. No lemmas are applied; the body is the formula itself.
why it matters
This is the gauge summand in the algebraic edge TT decomposition. The main existence theorems write every symmetric $H$ as $H=H_{\mathrm{TT}}+\mathrm{gaugePart}(m,v)+\beta,P_\perp(m)$ with $H_{\mathrm{TT}}$ transverse-traceless, so the definition is the middle term of that identity (and of its primed existential form).
Downstream it feeds gaugeCorrected (subtract the gauge piece), the symmetry lemma for the gauge part, load identities, and the decoy longitudinal matrix used to show that pure-gauge modes fail transversality. It does not itself close continuum gravity recovery or flip gap_action_recovery; it only supplies the algebraic gauge generator required by the TT splitting on $\mathrm{Fin},4$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.