tOpIter_chain_homotopy_zero
plain-language theorem explainer
On degree-0 singular chains of a space X, the boundary of the k-fold prism operator equals the identity minus the k-fold barycentric subdivision: ∂ ∘ T_k = id − S^k. Algebraic topologists building Mayer–Vietoris or subdivision arguments for singular homology cite this telescoped homotopy identity. The proof is induction on k, using the single-step degree-0 homotopy and abelian cancellation.
Claim. For any topological space $X$ and any $k \in \mathbb{N}$, if $T_k$ is the $k$-fold prism (chain homotopy) operator in degree $0$, $S^k$ the $k$-fold barycentric subdivision operator on $C_0(X)$, and $\partial : C_1(X) \to C_0(X)$ the singular boundary, then $\partial \circ T_k = \mathrm{id}_{C_0(X)} - S^k$ as morphisms of abelian groups.
background
The module develops singular subdivision for Recognition Science foundations: chain groups $C_n(X)$ are presented as coproducts $\coprod_{\sigma} \mathbb{Z}$ over singular $n$-simplices (the Cgrp presentation), with boundary $\partial$ the usual singular differential out of degree $n+1$.
Barycentric subdivision induces a chain map $S$ on these groups; $S^k$ is its $k$-fold iterate. A prism operator $T$ supplies a chain homotopy between $\mathrm{id}$ and $S$ in positive degrees; $T_k$ is the telescoped sum of the first $k$ prism steps. In degree $0$ the complex has no incoming boundary from below, so the homotopy identity collapses to a pure telescoping relation between $\partial T_k$, the identity, and $S^k$.
Upstream, the single-step identity $\partial \circ T = \mathrm{id} - S$ in degree $0$ is already available, as are the recursive definitions of the iterates $T_{k+1}$ and $S^{k+1}$ and the fact that $S$ commutes with itself under composition.
proof idea
Induction on $k$.
Base $k=0$: both $T_0$ and $S^0$ are zero and identity respectively in the usual conventions of the module, so $\partial \circ 0 = 0 = \mathrm{id}-\mathrm{id}$.
Successor: expand $T_{k+1}$ and $S^{k+1}$ by their recursive clauses, push composition through the sum via preadditive bilinearity, apply the single-step degree-0 homotopy $\partial \circ T = \mathrm{id}-S$, feed in the inductive hypothesis, cancel the identity factors, and use $S^k \circ S = S^{k+1}$. The remaining formal difference of morphisms is discharged by abel.
why it matters
This is the degree-0 telescoped homotopy that lets subdivision act as a chain-level approximation to the identity. Downstream, sub_sdOpIter_eq_bnd_zero rewrites it elementwise as $z - S^k z = \partial(T_k z)$, the form needed when chasing individual chains through Mayer–Vietoris diagrams. The same identity feeds exists_asubIter_small, the Stage-6 payoff that iterated barycentric pieces of an affine simplex become uniformly small in the standard simplex metric.
In the Recognition foundation stack this is pure singular-homology scaffolding: it underwrites excision and local-to-global gluing for chain-level arguments that later connect to the eight-tick / Clifford bridge material, but it does not itself force $\varphi$, $D=3$, or the J-cost. It closes the algebraic half of the subdivision package so metric smallness can be promoted to homology isomorphisms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.