zeroWindingCycles_bound_of_directedCycleTerms
plain-language theorem explainer
Assuming every directed-cycle free term is homologous to an integer multiple of the fundamental cycle on S¹, every singular 1-cycle of winding zero is a 2-boundary. Algebraic topologists working the H₁(S¹)≅ℤ comparison cite this as the last reduction step from local cycle geometry to the zero-winding filling target. The proof is a one-line composition of two prior implications.
Claim. Assume decidable equality on singular $0$- and $1$-simplices of $S^1$. If every directed-cycle free term $t$ is homologous (in the singular integer chain complex of $S^1$) to an integer multiple of the fundamental cycle, then every singular $1$-cycle $z$ with winding number $W(z)=0$ is the boundary of some singular $2$-chain.
background
The module lifts path-level winding on $S^1$ to singular simplices and proves that displacement kills boundaries: for every singular $2$-simplex $F$, the alternating face sum of displacements vanishes. Combined with the fact that the once-around loop has winding $1$, this yields a winding homomorphism on $1$-cycles that is a left inverse to the fundamental class (the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$).
The remaining half is generation: every $1$-cycle should be homologous to an integer multiple of the fundamental cycle. The local geometric target directedCycleTerms_boundary_generate asks that each directed-cycle free term equal $\partial b + n\cdot\gamma$ for some $2$-chain $b$ and integer $n$. The global target fundamentalCycle_boundary_generates asks the same for arbitrary $1$-cycles. The zero-winding filling target then says: if $W(z)=0$, then $z$ is a pure boundary.
Singular $0$- and $1$-simplices are the actual vertices of Mathlib's singular simplicial set of TopCat.sphere 1; decidable equality on them is needed for free-module bookkeeping.
proof idea
One-line term-mode wrapper. First apply fundamentalCycle_boundary_generates_of_directedCycleTerms to the hypothesis, obtaining the global generation statement that every $1$-cycle is homologous to $n\cdot\gamma$ plus a boundary. Then feed that into zeroWindingCycles_bound_of_fundamentalCycle_boundary_generates, which writes $z=\partial b+n\cdot\gamma$, notes that winding kills boundaries and sends $\gamma$ to $1$, and concludes $W(z)=0$ forces $n=0$, hence $z=\partial b$.
why it matters
This declaration is the terminal reduction in the CircleWindingChain generation ladder: local directed-cycle filling implies global fundamental-cycle generation, which implies the zero-winding filling theorem. The module doc identifies the latter as the missing half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ once winding is known to kill boundaries and to send the fundamental loop to $1$.
No downstream consumers are wired yet (used_by is empty), so the theorem currently closes an internal geometric target rather than feeding a named parent. In the broader Recognition foundation it supplies the chain-level fact that zero-winding cycles bound, which is the singular-homology counterpart of the circle's fundamental class being a generator. The remaining open geometric work is to discharge the hypothesis itself: prove that each concrete oriented cyclic family is homologous to an integer multiple of $\gamma$, via subdivision/prism machinery Mathlib does not yet provide.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.