sum4
plain-language theorem explainer
For any real function on a four-element index set, the Finset sum equals the explicit four-term sum f(0)+f(1)+f(2)+f(3). Star-kernel assembly proofs cite it to expand the sum over the four (cube, Kuhn simplex) pairs that contain a fixed hinge. The proof is a short decidable enumeration of Finset.univ followed by sum_insert and ring.
Claim. For every $f:\{0,1,2,3\}\to\mathbb{R}$, $\sum_{m\in\{0,1,2,3\}} f(m)=f(0)+f(1)+f(2)+f(3)$.
background
The ambient module treats the type-(2,2) triangle hinge on the 4D periodic Freudenthal lattice (masks ${0,3,15}$, difference masks $(3,12)$) and its full star. Exactly four (cube translate, Kuhn simplex) pairs contain that hinge; the star class kernel is assembled by summing a per-member contribution over those four slots.
The same four-term expansion already appears in the sibling type-(1,2) star-kernel module. Both modules import the dihedral and flat hinge kernels plus the 15-class edge stencil, and never redefine that API. The lemma is pure finite-sum bookkeeping: it converts a Mathlib Finset.sum over Fin 4 into an ordinary four-term expression that later simp and fin_cases steps can discharge member-by-member.
proof idea
Rewrite Finset.univ on Fin 4 as the nested insert chain insert 0 (insert 1 (insert 2 (insert 3 ∅))), justified by decide. Then simp [Finset.sum_insert] peels the sum into four summands plus the empty-sum zero; ring cleans the resulting arithmetic identity. No gravity-specific lemmas are used.
why it matters
Parent theorem fullStarClassKernel_eq (both in this module and in the type-(1,2) sibling) rewrites the assembled star class kernel as the closed-form kernel by first applying this expansion, then evaluating each of the four star members. That equality is deliverable A.4 of the module: the full-star deficit class kernel on all 15 stencil classes for the (2,2) orbit, with flatness gate $4\cdot\arccos 0=2\pi$.
It sits inside the QG full-theory campaign after the (1,1) seed orbit. It does not close flat Hessian assembly over all hinges, nor S_RS_converges_EH_4d, nor gap_action_recovery. Within the Recognition forcing chain it is local discrete-geometry scaffolding toward continuum Einstein–Hilbert recovery, not a T0–T8 step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.