gaugeVector
plain-language theorem explainer
Defines the Euclidean gauge covector that cancels the longitudinal load of a symmetric 4×4 matrix against a nonzero wave covector m. Gravity analysts cite it when assembling the algebraic edge TT split H = TT + gauge + residual-trace. The body is a closed-form component formula: load over |m|² minus a longitudinal correction proportional to m.
Claim. For a wave covector $m \in \mathbb{R}^4$ and a matrix $H \in M_4(\mathbb{R})$, the gauge vector $v$ has components $$v_i = \frac{(Hm)_i}{|m|^2} - m_i \frac{(Hm)\cdot m}{2|m|^4},$$ where $|m|^2 = \sum_k m_k^2$ and $\cdot$ is the Euclidean inner product.
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 TT package (symmetry, Euclidean trace zero, Euclidean transversality) without a Frobenius pin; Lorentzian/null specialization is deferred.
Mat4 is $M_4(\mathbb{R})$. The load $w = Hm$ is the ordinary matrix-vector product. Momentum squared $s = |m|^2$ is the squared Euclidean norm of the wave covector. The local dot is the unweighted Euclidean pairing $\sum_i a_i b_i$.
The gauge part of a matrix is built from an outer-product style operator on a covector $v$; choosing $v$ so that $\mathrm{load}(\mathrm{gaugePart}(m,v), m) = Hm$ removes the longitudinal content before the TT projector is applied.
proof idea
Pure definition, no proof obligations. Componentwise, set $w := Hm$ and $s := |m|^2$, then return the vector with $i$-th entry $w_i/s - m_i,(w\cdot m)/(2s^2)$. The second term is the unique longitudinal correction that makes the subsequent gauge-part load identity hold when $s \neq 0$.
why it matters
Feeds the main algebraic closing theorems exists_edgeTTDecomposition and exists_edgeTTDecomposition', which state every symmetric $4\times 4$ matrix against nonzero Euclidean $m$ splits as TT + gauge + residual-trace part. Also drives gaugeCorrected, gaugeCorrected_symmetric, load_gaugePart_gaugeVector, and dot_gaugeVector, and is reused by the Lorentzian companion exists_lorentzTTDecomposition.
In the Recognition gravity stack this is the smallest kernel-checked increment toward edge TT structure on 4D lattices. Module docs are explicit that it does not yet decompose Regge EDGE perturbations, prove $S_{\mathrm{RS}}$ converges to Einstein-Hilbert in 4D, or flip gap_action_recovery. It sits upstream of continuum polarization counting ("two polarizations in 4D") once the Euclidean algebraic kernel is locked.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.