prism_sum_cancellation
plain-language theorem explainer
Alternating double sums of prism faces and face-prisms cancel under the three prism face identities, leaving only the two endpoint contributions. Algebraic topologists cite this as the discrete engine of Hatcher's prism-operator identity (Thm 2.10). The proof partitions the index lattice into below-diagonal, strip, and above-superdiagonal regions and matches each bulk region bijectively against the opposing sum.
Claim. Let $M$ be an abelian group and $n\in\mathbb{N}$. Suppose $G$ on $\mathrm{Fin}(n+2)\times\mathrm{Fin}(n+3)$ and $G'$ on $\mathrm{Fin}(n+2)\times\mathrm{Fin}(n+1)$ satisfy: $G(i+1,j)=G'(j,i)$ when $j\le i$; $G(i,j+1)=G'(j,i)$ when $i<j$; and $G(i,i+1)=G(i+1,i+1)$ on the superdiagonal. Then $\sum_{i,j}(-1)^{i+j}\,G(i,j)+\sum_{k,i'}(-1)^{k+i'}\,G'(k,i')=G(0,0)-G(n+1,n+2)$.
background
The SingularPrism module builds the prism operator on singular chains so a continuous homotopy $F:X\times I\to Y$ induces a chain homotopy between the endpoint chain maps. On each singular simplex the prism has faces that decompose into extruded original faces plus the two endpoint simplices; the signed boundary of that prism is the classical Hatcher identity.
Here $G$ abstracts the faces of the prisms ($\partial P$) and $G'$ the prisms of the faces ($P\partial$), both valued in an arbitrary abelian group. The three hypotheses are exactly the prism face-commutation relations: below-diagonal faces of $P$ match $P$ of faces one way, above-superdiagonal faces match the other way, and the two writings of each superdiagonal face agree.
After those relations are imposed, the two alternating double sums are forced to collapse to the pure endpoint difference $G(0,0)-G(\mathrm{last},\mathrm{last})$, i.e. the algebraic content of Hatcher's Theorem 2.10.
proof idea
Rewrite both nested sums as sums over product finsets, then split the $(i,j)$-lattice with the module's product-partition lemmas into the strict below-diagonal region, the diagonal-plus-superdiagonal strip, and the strict above-superdiagonal region (and the two complementary halves for $G'$).
A finset bijection identifies the below-diagonal $G$-sum with the negative of the $k\le i'$ half of the $G'$-sum, feeding the first face identity and a sign shift of $+1$. A second bijection does the same for the above-superdiagonal region against the $i'<k$ half. What remains of the strip is killed by the superdiagonal agreement hypothesis and telescopes to the two corner terms $G(0,0)-G(\mathrm{last},\mathrm{last})$.
why it matters
This is the pure additive cancellation step inside the positive-degree chain-homotopy identity $\partial\circ P+P\circ\partial=(F_1)\sharp-(F_0)\sharp$. That identity is what makes the forward map of a homotopy equivalence induce an isomorphism on singular homology.
In the Recognition Science mirror the singular-homology invariance package sits in Foundation as infrastructure: continuous deformations of recognition geometries must not change homology-level invariants. The lemma itself is classical algebraic topology (Hatcher 2.10), not an RS forcing step (T0–T8, RCL, $\varphi$); it closes the prism half of the homotopy-invariance scaffold so downstream modules can treat singular homology as a homotopy functor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.