sum_prod_partition
plain-language theorem explainer
Any sum of an M-valued function on Fin(n+2)×Fin(n+3) splits into four blocks: below the diagonal, on the diagonal, on the superdiagonal, and strictly above it. Algebraic topologists cite this when setting up the prism operator ∂P index set for singular homology. The proof is successive Finset filter splits, closed by omega and abel.
Claim. Let $M$ be an abelian group and $F:\mathrm{Fin}(n+2)\times\mathrm{Fin}(n+3)\to M$. Then $\sum_p F(p)$ equals the sum of four restricted sums over pairs $(i,j)$ with $j<i$, $j=i$, $j=i+1$, and $j>i+1$ respectively (comparing the underlying natural numbers).
background
The module develops the singular prism operator used to prove that homotopy equivalences induce isomorphisms on singular homology with integer coefficients. The prism $P$ on an $n$-simplex produces an $(n+1)$-chain whose faces involve a double index set $\mathrm{Fin}(n+2)\times\mathrm{Fin}(n+3)$ for the composite $\partial P$.
Comparing the two coordinates (as naturals) cuts that rectangle into four regions: strictly below the diagonal, the diagonal, the superdiagonal $j=i+1$, and strictly above the superdiagonal. The companion two-way partition of the $P\partial$ index set $\mathrm{Fin}(n+2)\times\mathrm{Fin}(n+1)$ appears nearby in the same file.
This is pure additive combinatorics on finite index sets; no topology enters until the face maps and prism identities are imposed downstream.
proof idea
Work classically. First split the full universe by the predicate $j<i$ via Finset.sum_filter_add_sum_filter_not. On the complementary filter $\neg(j<i)$, split again by $j=i$, leaving the region $j\ge i+1$. That remainder is itself split by $j=i+1$ versus $j>i+1$, again with sum_filter_add_sum_filter_not.
Each filter identity is discharged by filter_filter plus filter_congr with omega on the natural-number comparisons. The final rearrangement of the four summands is abel.
why it matters
Direct consumer is prism_sum_cancellation, which packages Hatcher's Theorem 2.10: under the three prism face identities, the signed double sums over $\partial P$ and $P\partial$ collapse to $G(0,0)-G(\mathrm{last},\mathrm{last})$, i.e. $g_\sharp-f_\sharp$. That cancellation is the algebraic engine behind homotopy invariance of singular homology in this development, feeding isIso_homology_map_of_homotopyEquiv.
In the Recognition Science foundation layer the lemma is scaffolding for the singular-homology toolkit, not a physics forcing step (T0–T8). It earns its place by making the prism double-sum bookkeeping fully machine-checked before any topological identification is applied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.