sum_prod_partition'
plain-language theorem explainer
Any sum of an M-valued function over the product index set Fin(n+2)×Fin(n+1) splits as the sum on the closed lower triangle (first coordinate ≤ second) plus the sum on the strict upper triangle (second < first). Algebraic topologists cite it when setting up prism-operator double sums for Hatcher's 2.10. The proof is a classical Finset filter split plus an omega check that the two predicates are complementary.
Claim. Let $M$ be an additive commutative group and $n\in\mathbb{N}$. For any $F:\mathrm{Fin}(n+2)\times\mathrm{Fin}(n+1)\to M$, $$\sum_{q} F(q)=\sum_{q_1\le q_2} F(q)+\sum_{q_2<q_1} F(q),$$ where the sums run over the indicated subsets of the finite product index set (coordinates read as natural numbers).
background
The module develops singular prism operators on topological spaces, the standard tool that proves homotopy invariance of singular homology (Hatcher, Algebraic Topology, Thm 2.10). A prism on an $n$-simplex is a continuous map $\Delta^n\times I\to X$; its faces and the prisms of faces produce two families of singular chains whose alternating double sums must cancel.
The index set for the "prism of faces" family $P\partial$ is the product $\mathrm{Fin}(n+2)\times\mathrm{Fin}(n+1)$. The geometric face identities split that product into a lower triangle (first index $\le$ second) and a strict upper triangle (second $<$ first). Those two regions are exactly the domains on which the two prism-face matching hypotheses of the cancellation lemma apply.
Sibling definitions supply the continuous prism map, its face operators, and the unit-interval second-coordinate projection. The present lemma is pure finite-sum bookkeeping: it does not yet impose signs or face relations, only the set-theoretic partition of the double index.
proof idea
Work classically so that decidable filters exist on the finite product. Rewrite the full sum via Finset.sum_filter_add_sum_filter_not applied to the predicate "first coordinate $\le$ second". The first summand is already the lower-triangle sum. For the second summand, apply Finset.sum_congr after Finset.filter_congr: on every index the negation of $q_1\le q_2$ is equivalent to $q_2<q_1$, which omega discharges. The resulting identity is definitional equality of the two filtered sums.
why it matters
Direct consumer is prism_sum_cancellation, the abstract form of Hatcher's alternating double-sum cancellation: once the three prism face identities hold, the signed sums over $G=\partial P$ and $G'=P\partial$ collapse to the single difference $G(0,0)-G(\mathrm{last},\mathrm{last})$, i.e. $g_\sharp-f_\sharp$. That cancellation is the algebraic heart of the prism operator argument.
The same partition is then used (via the cancellation lemma) on the path to isIso_homology_map_of_homotopyEquiv: the singular-homology functor sends a homotopy equivalence to an isomorphism of $\mathbb{Z}$-modules. In the Recognition Science foundation stack this supplies the topological invariance needed when singular chains and prism homotopies interface with the eight-tick / Clifford grading story, without yet touching the J-cost or forcing chain.
The lemma itself is elementary and fully proved; it closes a pure bookkeeping gap rather than an open physical claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.