classCoeff_sub
plain-language theorem explainer
The 4D Regge edge-class coefficient is additive under matrix subtraction: for any pair of 4×4 real matrices and any of the 15 Freudenthal displacement classes, the class load of A−B equals the difference of the loads. Anyone packaging a finite TT quadratic or polarization identity over edge classes will cite this. The proof is a one-line unfold of the class coefficient into edge load, then the existing edge-load subtraction lemma.
Claim. For all $4\times 4$ real matrices $A,B$ and every Freudenthal edge class $d\in\{0,\ldots,14\}$, the edge-class coefficient satisfies $c_d(A-B)=c_d(A)-c_d(B)$, where $c_d(H)=D_d^{\mathsf T} H D_d$ and $D_d\in\{0,1\}^4\setminus\{0\}$ is the displacement of class $d$.
background
This module is the 4D Regge edge-stencil layer in the QG campaign: fifteen nonzero Freudenthal displacement classes in ${0,1}^4$, indexed by Fin 15 via bit masks. For each class $d$ one forms the squared-length coefficient of a symmetric $4\times 4$ matrix $H$ against the class displacement $D_d$, written $c_d(H)=D_d^{\mathsf T} H D_d$. That is exactly the 3D polEdgeCoeff / 4D edge-load convention, specialized to the class displacement.
The definition is a thin wrapper: classCoeff H d is edgeLoad H (classDisp d). Upstream, edgeLoad is already known to be linear in the matrix argument; in particular edgeLoad_sub states edgeLoad(A-B,v)=edgeLoad(A,v)-edgeLoad(B,v) for any displacement $v:\mathrm{Fin},4\to\mathbb{R}$. The present result simply transports that identity to the class-indexed packaging used by the provisional finite TT quadratic $\sum_d c_d(H)^2$ (all-ones weights; true 4D Regge weights remain OPEN).
proof idea
One-line wrapper. Unfold classCoeff on both sides so the goal becomes an instance of edgeLoad_sub at the class displacement classDisp d. Apply edgeLoad_sub A B _ and close. No new algebra is done here; all ring work lives in the edge-load subtraction lemma (itself sub_eq_add_neg plus additivity and negation of edge load).
why it matters
In the 4D stencil, every finite quadratic and polarization identity is written in the class coefficients $c_d(H)$. Subtraction-linearity is the missing half of additivity (the sibling classCoeff_add covers sums), so differences of Hessians, gauge residuals, and TT-minus-trace comparisons can be pushed inside the sum without expanding $D^{\mathsf T}HD$ by hand.
The module doc is explicit about honest scope: this does not prove $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$, does not close the ledger name edge_tt_decomposition, and does not flip gap_action_recovery. True 4D Regge class weights (the lift of the 3D hinge factor) remain OPEN; the provisional aggregate uses weight 1 on every nonzero class. No downstream theorems currently depend on this declaration, so it is infrastructure for the next kernel-checked increments in the same file (plane-wave class perturbations, gauge-entry identities, nonvacuity decoys).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.