load_sub
plain-language theorem explainer
Load (matrix–covector contraction) is additive under matrix subtraction: load(A−B,m)=load(A,m)−load(B,m) componentwise on Fin 4. Anyone proving transversality of gauge-corrected or TT-projected 4×4 matrices cites this. The proof unfolds the sum definition and distributes subtraction over the finite sum.
Claim. Let $A,B$ be real $4\times 4$ matrices and let $m\in\mathbb{R}^{4}$. Writing $\mathrm{load}(H,m)_{i}:=\sum_{j} H_{ij}m_{j}$, one has $\mathrm{load}(A-B,m)_{i}=\mathrm{load}(A,m)_{i}-\mathrm{load}(B,m)_{i}$ for every index $i\in\{0,1,2,3\}$.
background
This module is the algebraic layer of the QG campaign lane edge_tt_decomposition: Euclidean transverse-traceless structure for symmetric real $4\times 4$ matrices against a nonzero wave covector on $\mathrm{Fin},4$. Conventions lift the 3D closer (symmetry, Euclidean trace, Euclidean transversality) without a Frobenius pin; Minkowski specialization is deferred.
The load map is the plain matrix–vector product: $(\mathrm{load},H,m){i}=\sum{j} H_{ij}m_{j}$. Transversality of a matrix $H$ against $m$ is exactly $\mathrm{load},H,m=0$. Gauge correction and the TT projector are built by subtracting rank-one and outer-square pieces from $H$, so linearity of load in its matrix slot is the bookkeeping step that turns those subtractions into vanishing loads.
proof idea
One-line wrapper. Unfold the definition of load to expose the finite sum $\sum_{j} H_{ij}m_{j}$. Then simp with sub_mul (distributes subtraction through the scalar product $H_{ij}m_{j}$) and Finset.sum_sub_distrib (pulls the difference outside the sum over $\mathrm{Fin},4$). No external lemmas beyond Mathlib arithmetic are required.
why it matters
This is the elementary linearity fact that lets the rest of the 4D TT algebra close. Downstream, load_transverseProjector rewrites load of the transverse projector as load(I) minus a scaled outer square and cancels; gaugeCorrected_transverse changes the goal to load of a difference and applies this theorem plus the gauge-part identity; ttProject_transverse chains the same pattern through the full TT projection.
In the Recognition gravity stack this sits inside Wave 4 / W4-1: pure linear algebra supporting the ledger name edge_tt_decomposition. It does not itself recover Einstein–Hilbert or flip gap-action recovery; it only makes the Euclidean TT projector and gauge correction well-behaved on $\mathrm{Fin},4$, which is the kernel-checked increment the module advertises.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.