sum6
plain-language theorem explainer
Expands a sum over the six indices of Fin 6 into the explicit six-term addition f(0)+⋯+f(5). Cited when assembling the type-(1,3) full-star deficit class kernel from its six Kuhn-simplex members. Proof rewrites the universe Finset as nested inserts, then applies Finset.sum_insert and ring.
Claim. For any real-valued function $f$ on a six-element index set, $\sum_{m=0}^{5} f(m) = f(0)+f(1)+f(2)+f(3)+f(4)+f(5)$.
background
The module treats the Regge 4D type-(1,3) periodic-lattice star deficit class kernel: the triangle hinge with absolute masks ${0,1,15}$ and its full periodic Freudenthal star of Kuhn simplices. Exactly six simplices in the origin unit cube contain the hinge; the star angle sum and deficit class kernel are assembled by summing contributions over those six members.
This lemma is a pure finite-sum bookkeeping fact: the universe of Fin 6 is the nested insert of ${0,1,2,3,4,5}$, so a sum over that universe equals the six-term explicit sum. An identical private lemma already exists in the type-(1,1) seed-orbit kernel module; the present copy supports the parallel assembly path for type (1,3).
No geometric content is claimed here. The six-fold count itself comes from the star enumeration (exactly six Kuhn simplices contain the hinge), which is proved separately in this module.
proof idea
Rewrite Finset.univ on Fin 6 as the nested insert of $0$ through $5$ into the empty set, discharged by decide. Then simp with Finset.sum_insert peels the sum into six summands plus the empty sum. Finish with ring to normalize the resulting real expression. No external geometric lemmas are used.
why it matters
Feeds fullStarClassKernel_eq in this module (and the parallel equality in the type-(1,1) star kernel): that theorem rewrites the assembled full-star class kernel as the six-member sum, then substitutes each member's closed evaluation. Without the expansion, the assembled-versus-table equality cannot be reduced by simp and ring.
In the QG full-theory campaign this sits inside deliverable A item 5 (full-star deficit class kernel on classes $(1,3,5,7,9,11,13)$ with values $(\pm\sqrt{3})$). It does not itself touch the open transport of the kernel to type $(3,1)$, nor flat Hessian assembly, nor $S_{\mathrm{RS}}\to$ Einstein–Hilbert convergence. It is pure arithmetic scaffolding for the six-simplex star sum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.