sum15_all
plain-language theorem explainer
Any real function on a 15-point index set has total sum equal to the explicit fifteen-term addition of its values. Gravity analysts cite it when evaluating full-star directional sums over the Regge edge-stencil classes. The proof decides that the finite universe is the nested insert of indices 0 through 14, then unfolds Finset summation and closes by ring.
Claim. For every $f:\{0,\ldots,14\}\to\mathbb{R}$, $\sum_{d=0}^{14} f(d)=f(0)+f(1)+\cdots+f(14)$.
background
This module treats the type-(1,2) triangle hinge in the 4D Freudenthal triangulation of the integer lattice: the representative hinge with masks 0,1,7 and difference masks (1,6), together with its full periodic star (two unit cubes, four incident 4-simplices). The campaign imports a fixed 15-class edge stencil and a committed Gram-projection cosine calculus; it never redefines those APIs.
Directional observables on the star are written as sums of a real weight over the fifteen stencil classes. Expanding that abstract Finset sum into a concrete fifteen-term expression is a recurring bookkeeping step before the class-kernel values ($\pm\sqrt{2}/2$ and related gates) can be substituted.
The same expansion appears in the companion type-(2,2) kernel module; both copies are pure finite-sum identities and do not encode curvature or dynamics.
proof idea
Rewrite the universe Finset on Fin 15 as the nested insert of the fifteen concrete indices 0 through 14 into the empty set; the equality is discharged by decide. Then simp with Finset.sum_insert peels the sum into successive head terms plus the empty sum. A final ring normalizes the resulting addition to the displayed right-hand side. No external lemmas beyond the Finset API are required.
why it matters
The lemma is the expansion step inside the full-star directional gates of this module: uniform-scale decoy (directional sum of the constant-1 weight equals $\sqrt{2}/2$) and homothety stationarity (directional sum of the natural class weights equals 0). The identical pattern is reused in the type-(2,2) star-kernel module for its own decoy and stationarity theorems.
Those gates sit inside deliverable A of the QG full-theory campaign: the full-star deficit class kernel on all 15 stencil classes for the (1,2) orbit, after star enumeration, flat cosine multiset, and the flatness gate (angle sum exactly $2\pi$). They do not yet assemble the flat Hessian over all hinge orbits, prove continuum EH recovery, or close gap-action recovery; the complement orbit (2,1) remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.