abnd_comp_ateeIter
plain-language theorem explainer
On affine (n+1)-chains, the k-fold barycentric chain homotopy T^k satisfies the telescoped identity ∂T^k + T^k∂ = id − S^k. Homological algebraists proving that iterated subdivision is chain-homotopic to the identity cite this. The argument is induction on k: the base step is the single-step prism identity, and the inductive step swaps S past ∂ via the chain-map law then regroups.
Claim. Fix an apex map $\mathrm{bary}$ assigning to each vertex tuple a point of $\alpha$. Let $\partial$ be the affine boundary on affine chains $AC(\alpha,-)$, let $T^k$ be the $k$-fold chain homotopy built from $\mathrm{bary}$, and let $S^k$ be the $k$-fold barycentric subdivision. Then for all $k,n\in\mathbb{N}$, $$\partial\circ T^k_{n+1}+T^k_n\circ\partial=\mathrm{id}-S^k_{n+1}$$ on $AC(\alpha,n+1)$.
background
Affine $n$-chains $AC(\alpha,n)$ are finitely supported $\mathbb{Z}$-linear combinations of vertex tuples $\mathrm{Fin}(n+1)\to\alpha$. The module builds the usual singular toolkit in this purely combinatorial setting: an affine boundary $\partial$ (here abnd), a barycentric subdivision operator $S$ (asub) driven by an apex map $\mathrm{bary}$, and a prism/chain-homotopy operator $T$ (atee) that witnesses $S\simeq\mathrm{id}$ in a single step.
Iterates $T^k$ and $S^k$ are defined by the obvious recurrence ($T^0=0$, $S^0=\mathrm{id}$, and $T^{k+1}=T+T^k\circ S$, likewise for $S$). The single-step identity $\partial T+T\partial=\mathrm{id}-S$ is already available as abnd_comp_atee; the companion fact that $S$ is a chain map ($\partial S=S\partial$) is abnd_comp_asub. The present statement is the telescoped form of those two facts on positive-degree chains.
Local setting is Stage 4–5 of Foundation.SingularSubdivision: algebraic subdivision and homotopy before geometric pushforward along affine maps of standard simplices.
proof idea
Induction on the iterate $k$.
Zero case: $T^0=0$ and $S^0=\mathrm{id}$, so both sides collapse to $0$ by the zero laws for composition and sub_self.
Successor case: expand $T^{k+1}$ and $S^{k+1}$ by their recurrences, distribute composition over addition, then swap $S$ past $\partial$ on the cross term via the chain-map identity abnd_comp_asub (associativity of LinearMap.comp). Regroup the eight summands into
$(\partial T+T\partial)+(\partial T^k+T^k\partial)\circ S$
by an abel calculation. Feed in the single-step identity abnd_comp_atee and the inductive hypothesis, replace $(\mathrm{id}-S^k)\circ S$ by $\mathrm{id}\circ S-S^k\circ S$, and finish with asubIter_comp_asub plus another abel.
why it matters
This is the algebraic engine that makes iterated barycentric subdivision chain-homotopic to the identity on affine chains. Without the telescoped form, one cannot pass from the single-step prism operator to the statement "$S^k\simeq\mathrm{id}$ for every $k$", which is what homology invariance and the comparison with singular homology need.
In the Recognition Science foundation stack the module sits under the discrete-to-continuum bridge: affine chains and their subdivision supply the combinatorial side of singular homology before geometric realization. The forcing chain (T0–T8) does not quote this lemma directly; it is infrastructure for later continuum and measure arguments rather than a named T-step. Downstream use sites are not yet wired (used_by is empty); the natural consumers are homology-invariance theorems and the Stage 5a pushforward/equivariance block that follows in the same file.
No open sorry remains: the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.