sub_sdOpIter_eq_bnd_zero
plain-language theorem explainer
In degree 0, every singular chain equals its k-fold subdivision plus a boundary: z − S^k z = ∂(T_k z). Algebraic topologists building the singular Mayer–Vietoris sequence cite this as the elementwise form of the telescoped subdivision homotopy at the bottom degree. The proof evaluates the operator identity id − S^k = ∂ ∘ T_k on z and rewrites composition and identity maps in ModuleCat.
Claim. Let $X$ be a topological space and $z$ a singular $0$-chain on $X$ with $\mathbb{Z}$ coefficients. For every $k \in \mathbb{N}$, $$z - S_X^{k}(z) = \partial\bigl(T_X^{k}(z)\bigr),$$ where $S_X^{k}$ is the $k$-fold iterate of the singular subdivision operator on $C_0(X)$ and $T_X^{k}$ is the associated telescoped prism homotopy $C_0(X) \to C_1(X)$.
background
The ambient module builds singular chain groups and the Mayer–Vietoris comparison for covers, using the coproduct presentation of chains. The degree-$n$ chain group $C_n(X)$ is the coproduct $\coprod_{\sigma} \mathbb{Z}$ over singular $n$-simplices; the boundary $\partial : C_{n+1}(X) \to C_n(X)$ is the differential of that complex.
Singular subdivision supplies an endomorphism $S$ of each $C_n(X)$ together with a prism operator $T : C_n(X) \to C_{n+1}(X)$ implementing a chain homotopy from the identity to $S$. Iterates are defined recursively: $S^{0} = \mathrm{id}$, $S^{k+1} = S^{k} \circ S$, and $T^{0} = 0$, $T^{k+1} = T + S \circ T^{k}$. The operator-level identity $\mathrm{id} - S^{k} = \partial \circ T^{k}$ in degree $0$ is already available as tOpIter_chain_homotopy_zero.
This lemma simply reads that identity on an arbitrary $0$-chain, which is the form needed when chasing elements through the small-chain inclusion and the Mayer–Vietoris long exact sequence.
proof idea
Start from the operator equality $\mathrm{id} - S^{k} = \partial \circ T^{k}$ on $C_0(X)$ given by tOpIter_chain_homotopy_zero. Apply both sides to the fixed chain $z$ via congrArg. Rewrite the left-hand side using that the identity morphism acts as the identity on elements, and the right-hand side using that composition of ModuleCat morphisms acts by function composition (ModuleCat.comp_apply). After these two rewrites the evaluated identity is exactly $z - S^{k} z = \partial(T^{k} z)$; take the symmetric form.
why it matters
The lemma is the degree-$0$ base case for the elementwise telescoped homotopy on boundaries (sub_sdOpIter_eq_bnd_of_boundary), which extends the same identity to every degree whenever the input chain is itself a boundary. That family feeds the proof that the inclusion of small chains induces an isomorphism on homology (smallι_isIso_homologyMap), the key comparison step in the singular Mayer–Vietoris apparatus of this foundation module.
Within Recognition Science the singular MV package sits in the Foundation layer that underwrites continuum limits and cover-based gluing arguments used later in the forcing chain. The result itself is pure algebraic topology: it does not invoke J-cost, $\varphi$, or the eight-tick octave, but it clears a necessary homology isomorphism so those continuum arguments can quote a fully formal MV sequence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.