asubIter
plain-language theorem explainer
The k-fold iterate of the affine subdivision operator on n-chains: identity at k=0, then left-compose one more subdivision step at each successor. Anyone proving chain-map or chain-homotopy identities for barycentric subdivision, or diameter-contraction bounds under iteration, cites this family of endomorphisms. The body is a one-line recursive match on the iteration count.
Claim. Fix a barycenter assignment $\mathrm{bary}$ sending each finite vertex tuple in $\alpha$ to a point of $\alpha$. For $k,n\in\mathbb{N}$, the $k$-th iterate $S^k_{\mathrm{bary},n}$ is the $\mathbb{Z}$-linear endomorphism of the group of affine $n$-chains on $\alpha$ defined by $S^0=\mathrm{id}$ and $S^{k+1}=S\circ S^k$, where $S$ is the single-step subdivision operator built from $\mathrm{bary}$.
background
Affine $n$-chains $\mathrm{AC},\alpha,n$ are finitely supported $\mathbb{Z}$-linear combinations of vertex tuples $\mathrm{Fin}(n+1)\to\alpha$. They form the chain groups on which the module builds an algebraic model of singular subdivision without topology on $\alpha$ itself.
The single-step operator $S=\mathrm{asub},\mathrm{bary},n$ subdivides each generator by inserting barycenters (via the supplied family $\mathrm{bary}$) and taking the usual alternating sum of subsimplices. The present definition packages the powers $S^k$ as a single family of chain endomorphisms, indexed by the iteration count $k$.
The surrounding module develops prism operators, boundaries, and support-diameter estimates for these affine chains, in the style of classical singular homology subdivision arguments (cf. the Mathlib singular-homology imports).
proof idea
Pure recursive definition by pattern-match on $k$. The zero case returns the identity linear map on $\mathrm{AC},\alpha,n$. The successor case left-composes the single-step subdivision operator $\mathrm{asub},\mathrm{bary},n$ with the already-constructed $k$-fold iterate. No lemmas are invoked; the recursion is the content.
why it matters
This family is the carrier for every iterated subdivision identity in the module. Downstream, $\partial\circ S^k=S^k\circ\partial$ (chain-map property), the telescoped homotopy $\partial T_k+T_k\partial=\mathrm{id}-S^k$, commutation $S^k\circ S=S\circ S^k$, and the diameter bound that $k$-fold subdivision multiplies pairwise distances by $(n/(n+1))^k$ while keeping vertices in the original hull, all quantify over $\mathrm{asubIter}$. Existence results that some iterate makes supports arbitrarily small also apply it directly. In the Recognition foundation layer this is scaffolding for controlled refinement of affine chains, not a physics forcing step (T0–T8), but it supplies the algebraic subdivision engine those geometric estimates rest on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.