asubIter_zero
plain-language theorem explainer
The zero-fold iterate of the affine subdivision operator on integer chains is the identity endomorphism. Anyone proving chain-map or chain-homotopy identities for iterated subdivision cites this as the induction base. The proof is definitional reflexivity from the recursive clause of the iterate.
Claim. For any barycenter map $\mathrm{bary}$ and any degree $n$, the $0$-th iterate of the subdivision operator equals the identity $\mathbb{Z}$-linear map on the free abelian group of abstract $n$-chains: $S^{0}_{n} = \mathrm{id}$.
background
The module develops singular and affine subdivision on abstract chains AC α n, the free $\mathbb{Z}$-module on $(n+1)$-tuples in a type $\alpha$. A barycenter operator supplies, in each dimension, a point from a vertex tuple; the single-step subdivision endomorphism asub is built from cones and faces using that barycenter.
The $k$-fold iterate asubIter bary k n is defined by recursion on $k$: the zero case is LinearMap.id, and the successor case composes one more asub on the left. Upstream, asubIter is documented as "the $k$-th iterate of the subdivision operator (as a family of chain endomorphisms)." The identity maps appearing in the dependency graph are the ordinary identity automorphism and the identity Peano homomorphism; here only the module identity on chains is used.
This sits in the Foundation layer that links singular homology machinery (Mathlib singular homology, module categories) to Recognition Science support-geometry arguments about diameter contraction under repeated subdivision.
proof idea
One-line definitional proof: rfl. The recursive definition of the iterate matches on $k=0$ to LinearMap.id, so the equality is judgmental and needs no further lemmas.
why it matters
Every induction on the iterate count bottoms out here. Downstream, abnd_comp_asubIter uses it to start the proof that $\partial\circ S^{k}=S^{k}\circ\partial$ ("the iterate is a chain map"). The telescoped homotopy identity abnd_comp_ateeIter likewise inducts from this base: $\partial T_{k}+T_{k}\partial=\mathrm{id}-S^{k}$. Commutation of subdivision with its iterates (asubIter_comp_asub) rewrites the zero case via this lemma and the unit laws for composition.
Geometrically, asubIter_support_bound quotes the zero iterate when stating that $k$-fold subdivision contracts pairwise distances by $(n/(n+1))^{k}$ while keeping vertices in the original hull. gen_comp_sdOpIter ties singular subdivision of a generator to affine evaluation of the iterated operator on the identity tuple, again inducting through $k=0$.
In the Recognition framework this is scaffolding for the singular-homology side of support control (stage-6 affine geometry), not a forcing-chain landmark (T5–T8) itself. It closes no open physics claim; it is bookkeeping that makes the chain-homotopy and diameter arguments compile.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.