sum15_support
plain-language theorem explainer
If a real function on the 15 edge classes vanishes off the seven full-star deficit indices {2,3,6,7,10,11,14}, its total sum collapses to the sum of those seven values. Gravity analysts cite it when evaluating directional derivatives of the full-star class kernel. The proof zeros the complementary eight-term sum by case split, then expands the universe as nested inserts and simplifies.
Claim. Let $f:\{0,\ldots,14\}\to\mathbb{R}$. If $f(d)=0$ whenever $d\notin\{2,3,6,7,10,11,14\}$, then $\sum_{d=0}^{14} f(d)=f(2)+f(3)+f(6)+f(7)+f(10)+f(11)+f(14)$.
background
The ambient module is the Regge 4D full periodic-lattice star deficit class kernel: the seed triangle hinge and its full Freudenthal star in the integer lattice (four unit cubes, six incident 4-simplices). Edge data are organized by a fixed 15-class stencil; the full-star deficit class kernel is supported exactly on classes $(2,3,6,7,10,11,14)$ with signed weights $(-1,-1,+1,-1,+1,+1,-1)$.
Directional probes of that kernel are written as sums $\sum_{d:\mathrm{Fin},15} K(d),w(d)$. Once off-support vanishing of $K$ is known, any such sum reduces to seven terms. An analogous support lemma exists for the odd-index orbit ${1,3,5,7,9,11,13}$ in the companion star-kernel module; the present statement is the even-orbit counterpart for this star.
proof idea
Classical mode. First prove the complementary sum over the Finset ${0,1,4,5,8,9,12,13}$ is zero: Finset.sum_eq_zero, then for each member fin_cases plus the seven off-support hypotheses (each discharged by decide). Rewrite Finset.univ as the nested insert of ${2,3,6,7,10,11,14}$ into that complement (equality by decide). Apply Finset.sum_insert repeatedly with the zero complementary sum, then ring to match the seven-term right-hand side.
why it matters
This is the arithmetic bottleneck for the full-star gates listed in the module deliverable: uniform-scaling decoy and homothety stationarity both rewrite their directional sums through this support collapse, then evaluate the seven kernel values. The same pattern appears in the companion Kernel13 module for the alternate orbit.
In the QG campaign it sits after the dihedral cosine kernel and before any claim that the RS action recovers Einstein–Hilbert in 4D. It does not itself touch the forcing chain (T5–T8) or the Recognition Composition Law; it is pure finite-sum bookkeeping that makes the star deficit class kernel usable in stationarity and decoy checks. Parent theorems: fullStar_homothety_stationary and fullStar_uniformScale_decoy in this module (and their Kernel13 twins).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.