zeroWindingCycles_bound_of_pathConeCorrection
plain-language theorem explainer
Under the path-cone residual correction hypothesis on oriented cyclic families, every singular 1-cycle of winding zero on the circle is a singular 2-boundary. Algebraic topologists finishing the Mathlib singular-chain computation of H₁(S¹;ℤ) ≅ ℤ would cite this filling step. The proof is a one-line composition: path-cone correction yields free-prism generation, which already implies the zero-winding bound.
Claim. Assume decidable equality on singular $0$- and $1$-simplices of $S^1$. If every oriented cyclic family admits a path-cone residual correction (a singular $2$-chain whose boundary equals the residual between the summed path-cone boundary and the free-prism boundary), then every singular $1$-cycle $z$ on $S^1$ with winding number zero is the boundary of some singular $2$-chain.
background
This module lifts the path-level winding/displacement invariant of the circle to singular simplices of $\mathrm{TopCat.sphere},1$. Displacement of a singular $1$-simplex is $2\pi$ times winding, obtained by reparameterizing $\Delta^1$ to the unit interval. The key identity is that displacement kills boundaries: for every singular $2$-simplex the alternating face sum of displacements vanishes, by telescoping inside the convex standard $2$-simplex and homotopy invariance of path displacement.
Together with the fact that the fundamental loop has winding $1$, this supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The converse (every $1$-cycle is homologous to an integer multiple of the fundamental cycle) is a generation/filling statement. The zero-winding filling target asserts precisely that every singular $1$-cycle of winding zero is a $2$-boundary.
The path-cone residual correction target asks, for each oriented cyclic family, for a $2$-chain whose boundary matches the residual between the summed path-cone boundary and the desired free-prism boundary. An upstream lemma converts that correction into free-coordinate prism generation.
proof idea
One-line term wrapper. Apply the free-prism form of the zero-winding bound to the free-prism generation statement obtained from the path-cone correction hypothesis via the upstream conversion lemma (path-cone correction implies free-prism generation for oriented cyclic families). No further case analysis or chain algebra is performed here.
why it matters
Closes the zero-winding filling theorem once the path-cone residual correction target is assumed, which the nearby module comment identifies as enough for the full Mathlib singular-chain computation of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. In the module's architecture this is the generation half complementary to the already-proved "winding kills boundaries" identity and the fundamental-loop normalization. No downstream consumers are wired yet in the dependency graph; the declaration sits as a terminal packing step in the CircleWindingChain checklist rather than a leaf used by a named parent theorem. It does not itself touch the Recognition forcing chain (T5–T8) or the RCL, but supplies the singular-homology infrastructure those geometric arguments rely on when the circle appears as a phase space.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.