sdOpIter_succ
plain-language theorem explainer
The successor rule for iterated singular barycentric subdivision: one more step is the previous iterate composed with a single subdivision map on $C_n(X)$. Anyone proving chain-map, homotopy, or small-span facts for $S^k$ cites this rewrite. The proof is pure definitional equality from the recursive clause of the iterate.
Claim. For any topological space $X$ and $n,k\in\mathbb{N}$, the $(k+1)$-st iterate of the singular barycentric subdivision operator on the degree-$n$ singular chain group equals the composite of the $k$-th iterate with one further subdivision: $S^{k+1}=S^k\circ S$.
background
In singular homology, barycentric subdivision $S$ is the chain-level operator that replaces each singular simplex by the sum of its barycentric children. Here sdOp X n is that operator as a morphism $C_n(X)\to C_n(X)$, built by descending the generator-wise affine subdivision.
The $k$-fold iterate is defined recursively: $S^0=\mathrm{id}$ and $S^{k+1}=S^k\circ S$. That recursive clause is exactly the content of this lemma. The ambient module develops the singular subdivision package (affine support geometry, cone and prism operators, and the telescoping chain homotopy $T_k$ with $\partial T_k+T_k\partial=\mathrm{id}-S^k$) needed for excision and Mayer–Vietoris arguments in the Recognition foundation stack.
proof idea
One-line term proof by rfl. The recursive equation is definitionally identical to the successor branch of the iterate definition, so no further lemmas are required.
why it matters
This is the basic rewrite that every induction on the subdivision depth uses. Downstream it powers additivity of iterates ($S^{a+b}=S^a\circ S^b$), preservation of the small span under $S^k$ (for Mayer–Vietoris covers), the chain-map identity $S^k\circ\partial=\partial\circ S^k$, commutation $S^k\circ S=S\circ S^k$, the generator-to-affine-support comparison, and the telescoped homotopy identity $\partial T_k+T_k\partial=\mathrm{id}-S^k$. Without the successor clause those inductions cannot fire. In the broader RS foundation it is scaffolding for the singular-homology side of the forcing chain, not a physics landmark itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.