minkowskiDot_gaugeVector
plain-language theorem explainer
For a non-null Minkowski wave covector m and a symmetric 4×4 matrix H, the Minkowski pairing of the Lorentzian gauge vector with m equals half the load pairing scaled by 1/(m·m). Gravity analysts working the non-null TT projector cite this identity when checking that the gauge part absorbs the longitudinal load. The proof expands the pairing as a Fin 4 sum, splits, and simplifies by field arithmetic.
Claim. Let $m:\mathbb{R}^4$ be a covector with Minkowski self-pairing $m\cdot m\neq 0$, and let $H$ be a real $4\times 4$ matrix. Write $w_i$ for the Lorentz load of $H$ on $m$ (the contraction of $H$ against the raised $m$). Then the Minkowski pairing of the gauge vector $v$ built from $m$ and $H$ against $m$ satisfies $v\cdot m = (w\cdot m)/(2\, m\cdot m)$.
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$ real matrices against a Minkowski wave covector on $\mathrm{Fin},4$, signature $(-+++)$. Covectors are lowered by default; index raising negates the time component. The Minkowski pairing is $a\cdot b=-(a_0)(b_0)+\sum_{k=1}^3 a_k b_k$, equivalently $\sum_j a_j(\mathrm{raise},b)_j$.
The Lorentz load of $H$ on $m$ contracts the second index of $H$ against the raised wave covector. In the non-null sector $m\cdot m\neq 0$, the gauge vector is the Euclidean-style formula with Minkowski replacements: $v_i=w_i/s-m_i(w\cdot m)/(2s^2)$ where $w$ is the load and $s=m\cdot m$. The Euclidean sibling in EdgeTTDecomposition4D uses the same shape with ordinary load and momentum-squared.
The identity here evaluates $v\cdot m$ in closed form. It is the algebraic step needed before showing that the gauge part of $H$ reproduces the full load when contracted against $m$.
proof idea
Introduce abbreviations $w=\mathrm{lorentzLoad}(H,m)$, $s=m\cdot m$, $d=w\cdot m$. Expand $v\cdot m$ via the sum form of the Minkowski pairing and the definition of the gauge vector, obtaining $\sum_i(w_i/s-m_i d/(2s^2))(\mathrm{raise},m)_i$.
Split the sum into two pieces. The first piece factors $s^{-1}$ out of the sum and collapses to $d/s$ by the definition of $d$. The second piece factors the scalar $d/(2s^2)$ and collapses $\sum_i m_i(\mathrm{raise},m)_i$ back to $s$, giving $s,d/(2s^2)$.
Subtract and clear denominators with field_simp (using $s\neq 0$) plus ring simplification to reach $d/(2s)$, which is the claimed right-hand side.
why it matters
Immediate consumer is lorentzLoad_gaugePart_gaugeVector: the load of the pure gauge part built from this gauge vector equals the original load componentwise. That is the non-null half of the statement that the gauge correction absorbs all longitudinal content of $H$ before the TT remainder is formed.
In the QG full-theory campaign this sits in the Lorentzian linear-algebra layer of the ledger name edge_tt_decomposition. It does not yet touch Regge edge perturbations, Einstein-Hilbert recovery, or polarization normalizations; those are explicitly out of scope for the module. Within Recognition Science gravity analysis it is bookkeeping for the non-null projector $P_{ij}=\eta_{ij}-m_i m_j/(m\cdot m)$, the Lorentzian analogue of the Euclidean TT split used when matching ledger edge modes to continuum spin-2 content.
No forcing-chain landmark (T5–T8, RCL, $\phi$) is invoked; the result is pure Minkowski linear algebra supporting the gravity bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.