ateeIter_succ
plain-language theorem explainer
The successor clause of the iterated subdivision homotopy equals the single-step homotopy plus the previous iterate composed with barycentric subdivision. Algebraic topologists proving prism identities on affine chains cite this when inducting on subdivision depth. The equality is definitional: it unpacks the recursive packaging of the telescope.
Claim. For any barycenter assignment and any $k,n\in\mathbb{N}$, the degree-$n$ iterated subdivision homotopy at step $k+1$ equals $T_n + T_k^{(n)}\circ S_n$, where $T$ is the single-step subdivision chain homotopy, $S$ is barycentric subdivision on affine chains, and $T_k$ is the $k$-fold telescope.
background
The module builds barycentric subdivision and its chain homotopy on affine singular chains $\mathrm{AC},\alpha,n$ (integer linear combinations of affine $n$-simplices in a convex set $\alpha$). The barycenter map supplies a point in each simplex and drives the cone recursion.
Barycentric subdivision $S$ is defined by $S(\sigma)=b_\sigma\cdot S(\partial\sigma)$ on generators ($S=\mathrm{id}$ in degree 0). The single-step homotopy $T$ is the companion cone recursion $T(\sigma)=b_\sigma\cdot(\sigma-T(\partial\sigma))$ ($T=0$ in degree 0). The iterate $T_k$ packages the telescope $T\circ(1+S+\cdots+S^{k-1})$ by the recursion $T_0=0$ and $T_{k+1}=T+T_k\circ S$, degreewise as linear maps $\mathrm{AC},\alpha,n\to\mathrm{AC},\alpha,(n+1)$.
Composition of those linear maps is ordinary $\mathrm{ModuleCat}$ composition (written $\circ$ / .comp on the maps).
proof idea
Pure definitional equality. The recursive clause of the iterate is literally $T_{k+1}^{(n)}:=T_n+(T_k^{(n)})\circ S_n$, so the stated identity is rfl against that match arm. No lemmas are applied.
why it matters
Feeds the induction step of the telescoped chain-homotopy identity: $\partial\circ T_k+T_k\circ\partial=\mathrm{id}-S^k$ on positive-degree affine chains (abnd_comp_ateeIter). That identity is the standard algebraic-topology fact that iterated barycentric subdivision is chain-homotopic to the identity, which underwrites subdivision arguments and singular-homology comparisons in the Foundation layer.
In the Recognition stack this sits under the singular-prism / subdivision toolkit imported from Mathlib's singular homology, not under the T0–T8 forcing chain itself. It is infrastructure: once the telescope identity is available, higher subdivision lemmas can treat $S^k\simeq\mathrm{id}$ without reopening the cone recursion.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.