sum_support4
plain-language theorem explainer
If a real function on the ten edge slots vanishes off indices 1, 3, 7 and 9, its sum over all ten equals the sum of those four values. Private support-reduction helper inside the Regge 4D full-star deficit kernel. Proof splits the universe into the four support points plus a complementary six-set, peels with sum_insert, zeros the remainder by case analysis, then abelianizes.
Claim. Let $f:\{0,\ldots,9\}\to\mathbb{R}$. If $f(e)=0$ whenever $e\notin\{1,3,7,9\}$, then $\sum_{e=0}^{9} f(e)=f(1)+f(3)+f(7)+f(9)$.
background
The ambient module builds the full periodic Freudenthal star of the seed triangle hinge ${0,e_0,e_0+e_1}$ in the 4D integer lattice: four containing unit cubes and six incident 4-simplices. Deliverable A enumerates that star, records the flat cosine multiset, proves the flatness gate (angle sum $2\pi$), and extracts the full-star deficit class kernel on classes $(2,3,6,7,10,11,14)$.
Edge data for the local stencil live on a ten-slot index set Fin 10. Several assembly maps for individual star members are sparse: they only load a handful of those slots. This lemma is the pure finite-sum bookkeeping step that collapses a ten-term sum once the complementary slots are known to vanish.
It sits downstream of the dihedral and flat kernels and the 15-class edge stencil, and does not redefine their APIs.
proof idea
Term-mode finite-set algebra. Rewrite Finset.univ on Fin 10 as the nested insert of indices $1,3,7,9$ into the complementary six-element set ${0,2,4,5,6,8}$ (discharged by decide). Apply Finset.sum_insert four times (each non-membership again by decide). The remaining sum over the six-set is zero: for each element, fin_cases plus the support hypothesis forces $f(e)=0$. Finish by abel to rearrange $f,1+f,3+f,7+f,9$ into the target order.
why it matters
Feeds the private evaluations member2_eval and member3_eval, which expand assembleStarMember for star members 2 and 3 into sparse linear combinations of the deficit classes $d\in{2,6,10,14}$ with coefficients $\pm 1/2$. Those expansions are steps toward the full-star deficit class kernel (values $(-1,-1,+1,-1,+1,+1,-1)$ on classes $(2,3,6,7,10,11,14)$) listed as deliverable A.4 of the module.
In the QG campaign this is bookkeeping inside the kernel-checked increment after ReggeHinge4DDihedralKernel. It does not touch the open hinge orbits, the flat Hessian assembly, S_RS_converges_EH_4d, or gap_action_recovery. No direct contact with the T0–T8 forcing chain or RCL; the link is only through the Regge lattice layer of the gravity stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.