gaugePart
plain-language theorem explainer
Symmetric gauge contribution built from a wave covector m and a gauge vector v: the matrix with entries m_i v_j + v_i m_j. Anyone subtracting pure-gauge pieces in the Lorentzian edge TT decomposition cites this. The body is the componentwise symmetrized outer product; no proof content.
Claim. For covectors $m,v\in\mathbb{R}^4$, define the gauge part as the symmetric $4\times 4$ real matrix $(G(m,v))_{ij}=m_i v_j+v_i m_j$.
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$ matrices against a Minkowski wave covector on $\mathrm{Fin},4$, including the null case. Signature is $(-,+,+,+)$; covectors are lowered by default.
Mat4 is simply $\mathrm{Matrix}(\mathrm{Fin},4,\mathrm{Fin},4,\mathbb{R})$. Lorentz transversality contracts the second index of $H$ against the raised wave covector; the metric-trace is $\eta^{ij}H_{ij}$. The Euclidean sibling in EdgeTTDecomposition4D uses the identical component formula for its gauge part.
In the decomposition, every symmetric $H$ is written as a TT piece plus this gauge part plus a residual transverse-trace multiple of the projector. The gauge vector $v$ is chosen so that subtracting $G(m,v)$ removes the longitudinal contamination.
proof idea
Pure definition: the matrix is specified componentwise by the symmetrized outer product $m_i v_j+v_i m_j$. No lemmas, no tactics. Identical body to the Euclidean gaugePart it reuses by name and shape.
why it matters
This is the algebraic gauge term in the ledger name edge_tt_decomposition. Downstream, exists_edgeTTDecomposition and exists_edgeTTDecomposition' write every symmetric $H$ as TT plus gaugePart m v plus a scalar times the transverse projector. gaugeCorrected is exactly $H$ minus this term evaluated at the canonical gauge vector. Decoy constructions (decoyLongitudinal, decoyLongitudinal_not_transverse) build pure-gauge matrices from it to show they fail transversality.
It sits in the QG full-theory campaign's Lorentzian linear-algebra layer only. It does not itself prove continuum recovery of Einstein-Hilbert, close gap_action_recovery, or attach physical polarization norms. Framework-wise it supports the algebraic scaffolding that later gravity lanes need when separating physical TT modes from pure gauge on the eight-tick / $D=3$ side, but the present file stays strictly at the $4\times 4$ matrix level.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.