load
plain-language theorem explainer
The load of a real 4×4 matrix on a covector is the ordinary matrix–vector product: component i is the sum over j of H_ij m_j. It is the linear action used throughout the 4D edge transverse-traceless algebraic layer (transversality, gauge part, projectors). The body is a one-line Finset sum; no proof content.
Claim. For a real $4\times 4$ matrix $H$ and a covector $m\in\mathbb{R}^{4}$, define the load vector by $(\mathrm{load}(H,m))_{i}=\sum_{j} H_{ij} m_{j}$ for each index $i\in\{0,1,2,3\}$.
background
This module is the algebraic layer of the QG campaign item edge_tt_decomposition: linear-algebra TT structure for symmetric real $4\times 4$ matrices against a nonzero Euclidean wave covector on Fin 4. Conventions lift the 3D closer (Euclidean trace, Euclidean transversality, symmetry) without a Frobenius pin; Minkowski/null specialization is deferred.
Mat4 is the abbreviation for real $4\times 4$ matrices. Sibling notions (symmetry, Euclidean trace, tracelessness, transversality, the TT predicate, gauge part, outer square, transverse projector) all speak in terms of how such a matrix acts on the wave covector. The load is exactly that action: the image vector $H\cdot m$.
The dependency edges named H point at the RS cost reparametrization $H(x)=J(x)+1=\tfrac12(x+x^{-1})$ from the cost algebra. That is a different symbol; here the binder H is only the matrix argument.
proof idea
Definition only. The body is the componentwise matrix–vector product
fun i => ∑ j : Fin 4, H i j * m j,
i.e. the standard sum over the second index. No lemmas, no tactics, no hypotheses.
why it matters
Load is the primitive linear map that every TT conjunct reads: transversality is a statement about load against the wave covector, the gauge part and transverse projector are built from outer products and loads, and the TT predicate packages symmetry, tracelessness, and vanishing load in the momentum direction.
It sits in the smallest kernel-checked increment of Wave 4 / lane W4-1 and is referenced from dozens of downstream sites (about forty uses in the graph), including alpha-genesis calibration and residual-target lemmas that speak of gap, spectral, and closing loads in the $\alpha^{-1}$ forcing chain. Those parents consume the same linear-action vocabulary when they attenuate channel budgets and close residual targets against CODATA.
It does not itself flip continuum gravity closers (S_RS_converges_EH_4d, gap_action_recovery); it only supplies the 4D algebraic verb those layers need.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.