load_gaugePart_gaugeVector
plain-language theorem explainer
Against a nonzero Euclidean momentum on Fin 4, the longitudinal load of the pure-gauge matrix built from the canonical gauge vector of a 4×4 matrix H equals the load of H itself, componentwise. Anyone proving that the gauge-corrected matrix is transverse cites this identity. The proof expands the gauge-vector formula, applies the load-of-gaugePart lemma, and cancels by field_simp/ring.
Claim. Let $m\in\mathbb{R}^4$ satisfy $m\cdot m\neq 0$, and let $H$ be a real $4\times 4$ matrix. Write $v$ for the canonical gauge vector of the pair $(m,H)$. Then for every component $i\in\{0,1,2,3\}$, the longitudinal load of the pure-gauge matrix built from $v$ equals the longitudinal load of $H$: $\mathrm{load}(\mathrm{gaugePart}(m,v),m)_i=\mathrm{load}(H,m)_i$.
background
This module is the algebraic layer of the QG campaign item edge_tt_decomposition: the linear-algebra transverse-traceless split 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/null specialization is deferred.
Here $\mathrm{Mat4}$ is $\mathrm{Matrix}(\mathrm{Fin},4)(\mathrm{Fin},4),\mathbb{R}$. The Euclidean dot is $\sum_i a_i b_i$, and $\mathrm{momentumSq},m=m\cdot m$. The load of a matrix $H$ against $m$ is the longitudinal contraction (the object that vanishes precisely when $H$ is transverse to $m$). The pure-gauge matrix $\mathrm{gaugePart}(m,v)$ is the elementary longitudinal correction built from a covector $v$; the canonical choice $v=\mathrm{gaugeVector}(m,H)$ is the unique quadratic formula that matches the load of $H$.
Upstream in-module facts used below are the closed-form load of a gauge part and the identity $\mathrm{dot}(\mathrm{gaugeVector},m,H,m)=(\mathrm{dot},w,m)/(2s)$ with $w=\mathrm{load},H,m$ and $s=m\cdot m$.
proof idea
Introduce abbreviations $w:=\mathrm{load},H,m$, $s:=\mathrm{momentumSq},m$, $v:=\mathrm{gaugeVector},m,H$. Invoke the already-proved load formula for a pure-gauge matrix, $\mathrm{load}(\mathrm{gaugePart},m,v),m,i=s,v_i+m_i,(\mathrm{dot},v,m)$, and the companion identity $\mathrm{dot},v,m=(\mathrm{dot},w,m)/(2s)$ from dot_gaugeVector.
Unfold the defining component formula $v_i=w_i/s-m_i,(\mathrm{dot},w,m)/(2s^2)$. The algebraic key step is $s,v_i+m_i,(\mathrm{dot},v,m)=w_i$, discharged by rewriting the two identities above, then field_simp (using $s\neq 0$) and ring. Substitute back into the load-of-gaugePart expansion to finish.
why it matters
This is the load-matching lemma that makes the gauge correction cancel the longitudinal part of $H$. The sole immediate consumer is gaugeCorrected_transverse, which shows $\mathrm{IsTransverse},m,(\mathrm{gaugeCorrected},m,H)$ by rewriting
$\mathrm{load}(\mathrm{gaugeCorrected},m,H),m,i$
via load_sub and this identity to $w_i-w_i=0$.
In the Recognition gravity stack this sits inside Wave 4 / lane W4-1, the smallest kernel-checked increment toward the ledger name edge_tt_decomposition. It does not yet touch continuum Einstein-Hilbert recovery or the gap-action flip; it only closes the pure linear-algebra step that any later 4D TT polarization argument must quote. Framework landmarks T7/T8 (eight-tick octave, $D=3$) are ambient context for why a 4D Euclidean split is the right algebraic target, but this lemma itself is dimension-fixed linear algebra on $\mathrm{Fin},4$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.