bounds_of_isZero
plain-language theorem explainer
If the first singular homology of a space W vanishes as a module, every 1-cycle is a boundary. Algebraic topologists cite this when converting an H₁ = 0 hypothesis into an explicit filling of a cycle by a 2-chain. The proof is a one-line composition: the homology class is zero because the group is a zero object, and the class-zero criterion supplies the bounding chain.
Claim. Let $W$ be a topological space. If the singular homology $H_1(W;\mathbb{Z})$ is the zero module, then every $1$-cycle $z\in C_1(W)$ (i.e.\ every $1$-chain with $\partial_0 z=0$) is a boundary: there exists $w\in C_2(W)$ with $z=\partial_1 w$.
background
The ambient module works with singular chain groups $C_n(W)$ (coproducts of $\mathbb{Z}$ indexed by singular $n$-simplices) and the singular chain complex $SC(W)$. The boundary maps $\partial_n:C_{n+1}(W)\to C_n(W)$ are written bnd, and $H_n(W)$ is the homology of that complex.
A $1$-chain $z$ is a cycle when $\partial_0 z=0$. Its homology class is zero precisely when $z$ bounds some $2$-chain; that equivalence is recorded by the sibling lemma cls_eq_zero_iff. Separately, any element of a zero object in ModuleCat is the zero element (eq_zero_of_isZero).
The local setting is the arc-complement acyclicity development: one needs to turn vanishing of $H_1$ on complements into concrete fillings of cycles, as a step toward Hatcher's arc case of complement acyclicity in $S^D$.
proof idea
Term-mode one-liner. Apply eq_zero_of_isZero to the homology class of $z$ in the zero module $H_1(W)$, obtaining that the class is zero. Feed that equality into the forward direction of cls_eq_zero_iff, which converts a vanishing class into existence of a $2$-chain $w$ with $z=\partial_1 w$. No further case analysis or diagram chasing is required.
why it matters
Feeds the parent theorem arcComplementsAcyclic: every topological embedding of the unit interval into $S^D$ has $H_1$-acyclic complement, in every dimension $D$ (Hatcher 2B.1, arc case, formal). That theorem proceeds by contradiction on non-vanishing $H_1$ of the complement; this lemma is the algebraic hinge that turns an IsZero H_1 hypothesis into an explicit bounding chain.
In the Recognition Science foundation layer this is plumbing for high-dimensional linking and complement arguments that underwrite the forcing chain's geometric side (spatial dimension $D=3$, eight-tick structure). It does not itself force a physical constant; it closes a homology gap needed by the arc-complement package imported from LinkingVanishingHighDim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.