gaugePart_zero
plain-language theorem explainer
The Euclidean 4D gauge matrix built from any wave covector m and the zero vector field is the zero matrix. Anyone working the Regge edge TT attachment or gauge-corrected projections cites this as the base case. The proof is a two-line pointwise simplification of the bilinear definition of the gauge part.
Claim. For every wave covector $m \in \mathbb{R}^4$, the gauge matrix associated to the zero vector field vanishes: $\mathrm{gauge}(m,0)_{ij} = m_i \cdot 0 + 0 \cdot m_j = 0$ for all $i,j \in \{0,1,2,3\}$.
background
This module sits in the QG full-theory campaign (Wave 4 / lane W4-1), attaching the algebraic Euclidean $4\times 4$ TT / gauge / transverse-trace split to plane-wave edge loadings on axis edges of the 4-torus. The quadratic-form convention matches the 3D chain: edge load of a matrix $H$ along an axis displacement is the corresponding diagonal entry.
The gauge part is the symmetric bilinear matrix $(\mathrm{gaugePart}, m, v)_{ij} = m_i v_j + v_i m_j$ imported from the EdgeTTDecomposition4D layer (and its Lorentz twin). It is the discrete avatar of a Lie derivative contribution along a vector field $v$ at momentum $m$. Setting $v=0$ is the trivial gauge orbit, needed whenever one shows that an already-TT matrix is fixed by gauge correction.
proof idea
Pointwise extensionality on the $4\times 4$ matrix indices, then simp unfolds the definition of gaugePart. Each entry is $m_i\cdot 0 + 0\cdot m_j$, which reduces to $0$. No lemmas beyond the definition are required.
why it matters
Feeds directly into gaugeCorrected_eq_of_isTT: if $H$ is already transverse-traceless at momentum $m$ (with $m\neq 0$), the extracted gauge vector vanishes, and this lemma turns the residual gauge matrix into zero, so gauge correction leaves $H$ unchanged. That identity is part of the plane-wave edge TT attachment layer, which transports the algebraic TT decomposition onto axis-edge loadings and matches them to discrete Lie loadings. The module explicitly does not claim full edge_tt_decomposition, continuum Einstein-Hilbert recovery, or S_RS_converges_EH_4d; this lemma is a small exact algebraic step inside that honest scope.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.