sum_support2_29
plain-language theorem explainer
If a real-valued function on ten edge slots vanishes off indices 2 and 9, its total sum equals the sum of those two values. Star-member evaluators cite it to collapse local deficit kernels to the two nonzero stencil entries. The proof partitions the finite universe, drops the zero support by case analysis, and finishes by abelian cancellation.
Claim. Let $f:\{0,\ldots,9\}\to\mathbb{R}$. If $f(e)=0$ whenever $e\notin\{2,9\}$, then $\sum_{e=0}^{9} f(e)=f(2)+f(9)$.
background
The ambient module builds the full periodic-lattice star deficit class kernel for a seed triangle hinge in 4D Regge calculus: six incident 4-simplices across four unit cubes on the integer lattice, after the dihedral and flat kernels. Edge data live on a 10-slot local stencil; class kernels on the 15-class Freudenthal incidence layer are assembled by summing sparse local contributions.
The hypothesis is pure support control: $f$ may be nonzero only at slots 2 and 9. Downstream star-member assembly uses exactly this sparsity pattern when evaluating particular cube-translate members of the star. No curvature identity is claimed here; the lemma is finite-sum bookkeeping on Fin 10.
proof idea
Rewrite the universe of Fin 10 as the double insert of 2 and 9 into the complementary eight-element finset (discharged by decide). Apply Finset.sum_insert twice. The remaining sum is zero by Finset.sum_eq_zero: each residual index is discharged by fin_cases plus the support hypothesis. Close with abel to rearrange $f,2+f,9$ into the target order.
why it matters
Feeds the private evaluators member4_eval and member5_eval, which reduce assembleStarMember on star members 4 and 5 to explicit two-term class kernels (nonzero only on classes such as 11 with 3, or 11 with 7). Those evaluations sit inside deliverable A of the module: the full-star deficit class kernel on classes $(2,3,6,7,10,11,14)$ with values $(-1,-1,+1,-1,+1,+1,-1)$, plus the flatness gate (star angle sum $2\pi$) and the listed symmetry/scaling gates.
The module is an incremental QG kernel check after the dihedral kernel; it does not yet assemble the flat Hessian over all hinge orbits, prove $S_{\mathrm{RS}}$ converges to Einstein–Hilbert in 4D, or flip gap_action_recovery. This lemma is the sparse-sum step that keeps those member evaluations kernel-checked and axiom-light.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.