dot_gaugeVector
plain-language theorem explainer
For a nonzero Euclidean wave covector m on Fin 4 and any 4×4 real matrix H, the gauge vector built from H is half-aligned with m: its Euclidean inner product with m equals the load–momentum pairing divided by twice the squared momentum. Gravity analysts cite this when checking that the gauge correction removes the longitudinal load without residual projection error. The proof is a direct sum expansion with factoring and field simplification.
Claim. Let $m\in\mathbb{R}^{4}$ with $s:=\|m\|_{2}^{2}\neq 0$, and let $H$ be a real $4\times 4$ matrix. Write $w:=Hm$ for the load and $v$ for the gauge vector $v_{i}=w_{i}/s-m_{i}\,\langle w,m\rangle/(2s^{2})$. Then $\langle v,m\rangle=\langle w,m\rangle/(2s)$.
background
This module is the algebraic layer of the 4D edge TT decomposition (QG campaign lane W4-1). It lifts the 3D Euclidean TT package (symmetry, Euclidean tracelessness, transversality) to symmetric $4\times 4$ real matrices against a nonzero Euclidean wave covector on $\mathrm{Fin},4$. Minkowski/null specialization is deferred.
Local primitives: $\mathrm{Mat4}$ is $4\times 4$ real matrices; $\mathrm{momentumSq}(m)=\sum_{i}m_{i}^{2}$; $\mathrm{load}(H,m)=Hm$; $\mathrm{dot}$ is the standard Euclidean pairing. The gauge vector is the unique linear combination of $w=Hm$ and $m$ that will later cancel the longitudinal part of $H$ under the symmetric outer map $\mathrm{gaugePart}(m,v){ij}=m{i}v_{j}+v_{i}m_{j}$.
The identity here is elementary linear algebra on those sums; it does not invoke the Recognition cost $J$ or $H=J+1$, despite shared name collisions elsewhere in the monolith.
proof idea
Tactic proof by local abbreviations $w=\mathrm{load},H,m$, $s=|m|^{2}$, $d=\langle w,m\rangle$. Expand $\langle v,m\rangle$ by unfolding the gauge-vector formula, then split the sum into two pieces via $\mathrm{sub_mul}$ and $\mathrm{sum_sub_distrib}$.
The first sum factors as $d/s$ by pulling $s^{-1}$ out of the Finset sum. The second sum rearranges to $\sum m_{i}^{2}\cdot(d/(2s^{2}))=s,d/(2s^{2})$. Subtracting and applying $\mathrm{field_simp}$ with $s\neq 0$ yields $d/(2s)$, which rewrites as the claimed right-hand side.
why it matters
Feeds the immediate parent $\mathrm{load_gaugePart_gaugeVector}$, which shows that applying the gauge part built from this gauge vector recovers the full load: the longitudinal component of $H$ is exactly cancelled in the matrix–vector sense. That cancellation is the first half of the algebraic TT projector (gauge correction, then residual-trace subtraction against the transverse projector).
In the Recognition gravity stack this is kernel-checked scaffolding for $\mathrm{edge_tt_decomposition}$, not yet continuum Regge EDGE perturbations, $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$, or $\mathrm{gap_action_recovery}$. It inherits the Euclidean conventions of the 3D $\mathrm{IsTTPolarization}$ chain and keeps the expected axiom footprint classical only. No forcing-chain landmark (T5–T8, RCL, $\varphi$) is touched; the result is pure 4D linear algebra supporting later polarization counting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.