sum10
plain-language theorem explainer
Expands a sum over the ten indices of a 4-simplex edge/hinge labeling into an explicit ten-term sum, for any additive commutative monoid. Anyone evaluating the flat Schläfli summand table column-by-column cites this. The proof rewrites the Fin 10 universe as an explicit set, peels successive inserts down to a singleton, and finishes by abelian normalization.
Claim. For any additive commutative monoid $R$ and any map $f:\{0,\ldots,9\}\to R$, $$\sum_{h=0}^{9} f(h)=f(0)+f(1)+f(2)+f(3)+f(4)+f(5)+f(6)+f(7)+f(8)+f(9).$$
background
The ambient module treats the Freudenthal (Kuhn) 4-simplex at the combinatorial level $n_H=n_E=10$: ten squared-edge coordinates and ten triangle hinges. It mirrors the 3D Gate-A2 closed-form input (six edges, six hinges) one dimension up, and aims at a non-vacuous flat Schläfli identity with strictly positive hinge areas.
Sums over Fin 10 appear throughout the flat summand table (one row per hinge, one column per edge). Expanding such a sum into a concrete ten-term expression is a bookkeeping step before norm_num or case analysis on the edge index can fire.
The only local prior is the companion fact that the universe of Fin 10 equals the explicit set ${0,1,\ldots,9}$.
proof idea
Rewrite the sum domain via the explicit-universe lemma for Fin 10. Then repeatedly replace Finset.sum_insert (each insert-membership discharged by decide) until only a singleton remains; collapse that with Finset.sum_singleton. Finish with abel, which reassociates and reorders the resulting monoid sum into the written left-to-right order $f,0+\cdots+f,9$.
why it matters
Immediate consumer is the flat closed-form theorem: for every edge index $e$, the column sum $\sum_h$ of the flat Schläfli summand table vanishes. That theorem rewrites via this expansion, then cases on $e$ and simplifies each of the ten concrete terms by norm_num.
In the module tier list this sits under THEOREM material: Freudenthal 4-simplex combinatorics, flat hinge areas, and vanishing column sums of the flat summand table. It is pure scaffolding arithmetic for Gate-A2-style flat directional Schläfli kill; it does not touch the open pathwise identity off the flat seed, elevation to a candidate, or $S_{RS}\to$ Einstein–Hilbert convergence in 4D.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.