asubIter_comp_asub
plain-language theorem explainer
The algebraic barycentric subdivision operator on singular chains commutes with each of its finite iterates. Anyone assembling the telescoped prism homotopy for singular homology cites this when rearranging S^k past a single S. The proof is a short induction on the iterate count, using the recursive definition of the iterates and associativity of linear-map composition.
Claim. Fix a barycenter map $\mathrm{bary}$ and degrees $k,n\in\mathbb{N}$. Writing $S$ for the algebraic subdivision operator on degree-$n$ chains and $S^k$ for its $k$-fold iterate, one has $S^k\circ S=S\circ S^k$ as linear maps on the algebraic chain module.
background
The module builds algebraic singular-chain operators (boundary, cone, subdivision) over a coefficient type $\alpha$, in the style of the classical barycentric subdivision used to prove homotopy invariance of singular homology. The parameter bary is a choice of barycenter for each finite vertex tuple; the operator $S$ (written asub) is the induced linear endomorphism of the degree-$n$ algebraic chain module, and $S^k$ (asubIter) is defined by iterating $S$.
Composition here is ordinary composition of LinearMaps on those chain modules. The identity and unit laws for that composition (and the recursive clauses asubIter_zero, asubIter_succ) are the only algebraic input. Downstream, the same operators feed the prism/cone operators that produce chain homotopies between $S^k$ and the identity.
proof idea
Induct on the iterate count $k$.
- Zero case: $S^0$ is the identity map, so both sides reduce to $S$ by the unit laws
LinearMap.comp_idandLinearMap.id_compafter unfoldingasubIter_zero. - Successor case: unfold
asubIter_succ(so $S^{k+1}=S\circ S^k$), reassociate withLinearMap.comp_assoc, apply the inductive hypothesis $S^k\circ S=S\circ S^k$, then reassociate back.
No geometric content is used; the argument is pure endomorphism algebra.
why it matters
The sole recorded consumer is abnd_comp_ateeIter, the telescoped chain-homotopy identity $\partial\circ T_k+T_k\circ\partial=\mathrm{id}-S^k$ on positive-degree algebraic chains. That identity is the algebraic engine behind barycentric subdivision arguments in singular homology: once $S$ commutes with its iterates, the finite telescope of prism operators collapses cleanly to $\mathrm{id}-S^k$.
In the Recognition Science stack this sits in Foundation, supplying the singular-homology toolkit used to connect discrete recognition structure to continuum topology. It does not itself touch the forcing chain (T0–T8), the J-cost, or the $\varphi$-ladder; it is infrastructure those continuum comparisons rely on when homology is invoked.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.