classCoeff_add
plain-language theorem explainer
Edge-class coefficients on the 4D Freudenthal stencil are additive in the metric perturbation: for any two 4×4 matrices and any of the 15 nonzero {0,1}^4 displacement classes, c_d(A+B)=c_d(A)+c_d(B). Anyone building the provisional finite TT quadratic, its polarization identity, plane-wave class perturbations, or class-dot assemblies cites this. Proof is a one-line unfold of the class coefficient into edge load, then the existing edge-load additivity lemma.
Claim. For all $4\times 4$ real matrices $A,B$ and every Freudenthal edge class indexed by $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^\top H D_d$ and $D_d$ is the nonzero $\{0,1\}^4$ displacement vector of class $d$.
background
This module is the 4D Regge edge stencil: fifteen Freudenthal-style edge classes (nonzero displacements in ${0,1}^4$, indexed by bit masks) together with a provisional finite TT quadratic built from those classes. It is the next kernel-checked increment after the 4D edge-load attachment layer, mirroring the 3D chain's finite TT edge-class packaging.
The edge-class coefficient is defined by $c_d(H)=D_d^\top H D_d$, the same quadratic form convention as the 3D polarized edge coefficient and the 4D edge load. Concretely it is the edge load of $H$ on the class displacement $D_d$. The upstream lemma already records that edge load is additive in the matrix: $\mathrm{edgeLoad}(A+B,D)=\mathrm{edgeLoad}(A,D)+\mathrm{edgeLoad}(B,D)$ by expanding the bilinear form and distributing the finite sum.
The module is explicit that class weights are provisional (all-ones on every nonzero class). True 4D Regge Hessian weights at flat remain OPEN and must not be reverse-engineered from the Einstein-Hilbert answer.
proof idea
One-line wrapper. Unfold the definition of the class coefficient (it is edge load on the class displacement), then apply the upstream edge-load additivity theorem at that displacement. No extra algebra is needed: additivity of $c_d$ is exactly additivity of the underlying quadratic form $D^\top H D$ in $H$.
why it matters
This is the elementary linearity step that lets every higher stencil aggregate inherit additivity in the metric perturbation. Downstream it is used to prove left-additivity of the finite TT bilinear form, the exact quadratic expansion / polarization identity for the provisional finite TT quadratic, additivity of plane-wave class perturbations, and additivity of the class-dot pairing in the flat 4D Hessian assembly.
In the Recognition gravity campaign it sits inside the QG full-theory ladder after edge TT attachment, packaging 4D edge classes the way the 3D chain packaged polarized edge coefficients. It does not close the OPEN weight problem, nor does it claim convergence of the RS action to Einstein-Hilbert in 4D, full edge-TT decomposition, or gap-action recovery. It only makes the provisional all-ones aggregate algebraically well-behaved under matrix addition so polarization and gauge-entry identities can be stated exactly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.