edgeLoad_decomposition
plain-language theorem explainer
The edge load of a symmetric 4×4 matrix H on any displacement equals the sum of the loads of its TT projection, gauge part, and residual transverse-trace part, whenever the Euclidean wave covector is nonzero. Anyone transporting the algebraic edge TT split onto Regge axis-edge loadings cites this. The proof rewrites H by the algebraic decomposition and applies additivity of the load twice.
Claim. Let $H$ be a symmetric $4\times 4$ real matrix and $m\in\mathbb{R}^4$ a wave covector with $|m|^2\neq 0$. For every displacement $d\in\mathbb{R}^4$, the quadratic edge load of $H$ equals the sum of the edge loads of its TT projection against $m$, its gauge part built from the gauge vector of $(m,H)$, and its residual transverse-trace multiple of the transverse projector of $m$.
background
This module sits in the QG full-theory campaign (Wave 4 / lane W4-1): it attaches the Euclidean $4\times 4$ TT / gauge / transverse-trace split to plane-wave edge loadings on axis edges of the 4-torus, using the same quadratic-form convention as the 3D chain ($\mathrm{polEdgeCoeff},E,d=\sum_{ij}E_{ij}D^i D^j$).
The algebraic prior is exists_edgeTTDecomposition: every symmetric $4\times 4$ matrix against a nonzero Euclidean wave covector decomposes as TT + gauge + transverse-trace part. Explicitly, $H=\mathrm{ttProject}(m,H)+\mathrm{gaugePart}(m,v)+\tau,P_\perp(m)$ with $v$ the gauge vector of $(m,H)$ and $\tau$ the residual trace scalar. The gauge part is the symmetric rank-at-most-two matrix $(mv^T+vm^T)$.
edgeLoad is the bilinear quadratic form that sends a matrix and a displacement to the squared-length loading on that edge; siblings record that it is linear in the matrix (edgeLoad_add, edgeLoad_smul, edgeLoad_neg). On an axis edge the load collapses to the corresponding diagonal entry.
proof idea
Term-mode proof, three steps. First invoke the algebraic identity exists_edgeTTDecomposition m H hH hm and take its first conjunct, so $H$ equals the sum of the TT projection, the gauge part of the gauge vector, and the residual-trace multiple of the transverse projector. Rewrite only the outer $H$ on the left-hand side by that sum (a targeted conv_lhs so the projectors inside the right-hand summands are left alone). Finish by applying matrix-additivity of edgeLoad twice (edgeLoad_add). No further properties of TT or gauge are needed.
why it matters
This is the linearity bridge that moves the algebraic edge_tt_decomposition layer onto concrete Regge edge observables. Its sole recorded consumer is planeWaveAxisEdgePert_decomposition, which multiplies the same three-way split by the midpoint plane-wave phase $\cos(m\cdot x+m_a/2)$ and thereby decomposes the axis-edge plane-wave perturbation.
In the module's honest scope list this is item 2: "Linearity + decomposition transport." It does not close the ledger name edge_tt_decomposition in full (no 4D Regge action, no continuum Einstein-Hilbert recovery, no Freudenthal edge-class stencil), and it does not flip gap_action_recovery or prove $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$. It is the kernel-checked increment that makes the later exact finite-difference gauge identity (gauge part versus discrete Lie loading on axis edges) applicable termwise to each summand.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.