sum6
plain-language theorem explainer
The sum of a real-valued function over the six indices of Fin 6 equals the explicit six-term sum f(0)+…+f(5). Gravity analysts cite it when expanding the full Freudenthal star sum over the six incident 4-simplices. The proof rewrites the universe Finset as nested inserts and applies Finset.sum_insert plus ring.
Claim. For every function $f:\{0,1,2,3,4,5\}\to\mathbb{R}$, the sum $\sum_{m=0}^{5} f(m)$ equals the expanded sum $f(0)+f(1)+f(2)+f(3)+f(4)+f(5)$.
background
The ambient module builds the Regge 4D full periodic-lattice star deficit class kernel: the seed triangle hinge and its full Freudenthal star in the integer lattice, consisting of four containing unit cubes and six incident 4-simplices. Deliverable A of the module enumerates that star (exactly six cube-translate/Kuhn-simplex pairs) and assembles the full-star deficit class kernel on the fifteen edge classes.
Sums over those six star members are written as ∑ m : Fin 6, …. Expanding such a sum into an explicit six-term expression is a recurring bookkeeping step before evaluating each member's contribution (flat cosine, class kernel value, etc.). This private lemma packages that expansion once.
The same pattern appears in the sibling kernel module ReggeHinge4DStarKernel13, which carries an identical private expansion lemma used for the same purpose.
proof idea
Term/tactic hybrid, three steps. First rewrite Finset.univ : Finset (Fin 6) as the nested insert chain insert 0 (insert 1 (… insert 5 ∅ …)), justified by decide. Then simp [Finset.sum_insert] peels the sum into six summands plus the empty-sum zero. Finally ring normalizes the resulting arithmetic identity. No domain-specific lemmas are needed; the argument is pure finite-set bookkeeping.
why it matters
The lemma is the expansion step inside fullStarClassKernel_eq, which equates the assembled full-star class kernel (sum of six member evaluations) with the closed-form kernel on classes (2,3,6,7,10,11,14) with values (-1,-1,+1,-1,+1,+1,-1). That equality is deliverable A.4 of the QG full-theory campaign: the kernel-checked full-star deficit class kernel after the dihedral cosine calculus.
Downstream, the same expansion is reused in ReggeHinge4DStarKernel13.fullStarClassKernel_eq. Without the explicit six-term form, the member-wise evaluations (member0_eval through member5_eval) cannot be substituted and the class-by-class identity cannot be discharged by simp/ring.
It does not touch the forcing chain (T0–T8), RCL, or the alpha band; it is pure combinatorial scaffolding for the Regge star assembly. Open items flagged by the module (other hinge orbits, flat Hessian assembly, S_RS_converges_EH_4d, gap_action_recovery) remain untouched.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.