edgeLoad_sub
plain-language theorem explainer
The quadratic edge loading of a matrix difference equals the difference of the loadings: for 4×4 matrices A, B and any edge displacement d, load(A−B,d)=load(A,d)−load(B,d). Anyone transporting TT/gauge/trace splits or stencil class coefficients across differences of metric perturbations cites this. The proof is a three-line rewrite through additivity and negation, finished by ring.
Claim. For any $4\times 4$ real matrices $A,B$ and any displacement covector $d:\{0,1,2,3\}\to\mathbb{R}$, the quadratic edge loading satisfies $\mathrm{load}(A-B,d)=\mathrm{load}(A,d)-\mathrm{load}(B,d)$, where $\mathrm{load}(H,d)=\sum_{i,j}H_{ij}d_i d_j$.
background
This module sits in the QG full-theory campaign (Wave 4 / lane W4-1), one kernel-checked step past the algebraic 4D edge TT decomposition. 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 edge load itself is the bilinear form $\mathrm{edgeLoad},H,d=\sum_{i,j}H_{ij},d_i,d_j$ (equivalently $D^T H D$). Prior lemmas already establish additivity $\mathrm{edgeLoad}(A+B,d)=\mathrm{edgeLoad},A,d+\mathrm{edgeLoad},B,d$ and homogeneity under negation $\mathrm{edgeLoad}(-H,d)=-\mathrm{edgeLoad},H,d$ (the latter via scalar multiplication by $-1$). Subtraction is the remaining linear identity needed to move differences of metric matrices through the load map.
proof idea
Term-mode rewrite proof. Rewrite $A-B$ as $A+(-B)$ via sub_eq_add_neg, apply the already-proved additivity lemma edgeLoad_add, then the negation lemma edgeLoad_neg, and finish with ring to rearrange $X+(-Y)$ into $X-Y$. No unfolding of the double sum is required; the identity is pure linear algebra on the codomain $\mathbb{R}$.
why it matters
Linearity of the edge load under subtraction is the last elementary homomorphism fact before stencil-level class coefficients can be differenced. Downstream, classCoeff_sub in ReggeEdgeStencil4D is literally unfold classCoeff; exact edgeLoad_sub, so every 4D Freudenthal-style edge-class coefficient inherits difference-linearity from this lemma.
In the module's honest scope, this supports the "linearity + decomposition transport" bullet: edge load of $H$ equals the sum of loads of the TT, gauge, and residual transverse-trace parts, and therefore differences of those parts transport as well. It does not touch continuum Einstein-Hilbert recovery, the ledger name edge_tt_decomposition in full, or gap_action_recovery. Within Recognition gravity analysis it is bookkeeping infrastructure for the plane-wave attachment layer, not a forcing-chain landmark (T0–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.