ateeIter_zero
plain-language theorem explainer
The telescoped prism operator at iteration zero is the zero chain map in every degree. Algebraic topologists and anyone running the subdivision homotopy induction cite this as the base case of $T_k$. The proof is pure definitional unfolding of the recursive packaging $T_0=0$.
Claim. For every barycenter choice map and every degree $n$, the degree-$n$ component of the telescoped chain homotopy at iteration count zero is the zero $\mathbb{Z}$-linear map from the singular chain module in degree $n$ to the singular chain module in degree $n+1$.
background
The module builds singular subdivision and prism operators on free singular chains $AC_\alpha(n)$ over a convex ambient space $\alpha$. The elementary prism (homotopy) operator $T$ and the barycentric subdivision operator $S$ are packaged degreewise; their composites give the usual chain-homotopy relation $\partial T+T\partial=\mathrm{id}-S$ in positive degrees.
The iterated object $T_k$ is the telescoping sum $T\circ(1+S+\cdots+S^{k-1})$, written recursively by $T_0=0$ and $T_{k+1}=T+T_k\circ S$. Upstream, that recursion is exactly the definition of ateeIter: the $k=0$ branch is the zero map, and the successor branch adds one more prism after composing with subdivision.
proof idea
One-line definitional proof. The recursive definition of the telescoped operator sets the $k=0$ branch to the zero linear map, so equality to zero is rfl. No lemmas are applied.
why it matters
This is the induction base for the telescoped homotopy identity. Downstream, abnd_comp_ateeIter proves $\partial\circ T_k+T_k\circ\partial=\mathrm{id}-S^k$ on chains in degree $n+1$ by induction on $k$; the $k=0$ case collapses precisely because $T_0=0$ and $S^0=\mathrm{id}$, so both sides vanish. In the Recognition foundation stack this identity is the algebraic engine that lets barycentric subdivision act as a chain-homotopy equivalence, feeding continuum-limit and homology arguments built on singular chains rather than on ad-hoc discrete complexes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.