zeroWindingCycles_bound_iff_fundamentalCycle_boundary_generates
plain-language theorem explainer
Integer-valued winding already in hand, the two remaining geometric formulations of H₁(S¹;ℤ) ≅ ℤ are equivalent: every zero-winding 1-cycle bounds if and only if every 1-cycle is a 2-boundary plus an integer multiple of the fundamental cycle. Anyone assembling the generation half of the circle homology isomorphism cites this bridge. The proof is a two-direction constructor wiring the existing one-way implications, with integrality supplied by the directed-cycle kernel decomposition.
Claim. Assuming the free boundary kernel decomposes into directed cycles (hence winding is integer-valued on all singular $1$-cycles), the following are equivalent: (i) every singular $1$-cycle of winding $0$ is the boundary of some singular $2$-chain; (ii) every singular $1$-cycle $z$ admits $n\in\mathbb{Z}$ and a $2$-chain $b$ with $z = \partial b + n\,[S^1]$.
background
This module lifts path-level winding on $S^1$ to singular $1$-simplices via simplexDisplacement (displacement $= 2\pi\times$ winding after reparameterizing $\Delta^1$ to $[0,1]$). The key identity is that displacement kills boundaries: for every singular $2$-simplex the alternating face sum of displacements vanishes, by convexity of $\Delta^2$ plus homotopy invariance and additivity of path displacement. Together with the fact that the fundamental loop has winding $1$, this yields a left inverse $H_1(S^1;\mathbb{Z})\to\mathbb{Z}$.
Two residual geometric statements remain. Zero-winding bounding says every cycle of winding $0$ is a singular $2$-boundary. Fundamental-cycle generation says every $1$-cycle equals a $2$-boundary plus an integer multiple of the lifted fundamental cycle. Upstream, the free boundary kernel decomposes unconditionally into directed-cycle pieces (strong induction on $\ell^1$ size), which forces winding to be integer-valued on all singular $1$-cycles.
proof idea
Two-direction constructor.
Forward: from zero-winding bounding, apply fundamentalCycle_boundary_generates_of_integral_winding_of_zeroWinding_bounds. Integrality is obtained in one classical step by feeding the unconditional kernel decomposition freeBoundaryKernel_decomposesIntoDirectedCycles_holds into cycleWinding_integral_of_freeBoundaryKernel_decomposesIntoDirectedCycles. That lemma subtracts $n$ times the fundamental cycle (with $n=$ winding) and fills the zero-winding remainder.
Reverse: one-line application of the already-proved converse zeroWindingCycles_bound_of_fundamentalCycle_boundary_generates.
why it matters
This is the clean equivalence that collapses the two remaining geometric formulations of the generation half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ once integrality is free. Downstream, directedCycleFreeTermList_boundary_generates lifts termwise generation to finite directed-cycle lists, packaging the oriented-family target used in the circle $H_1$ computation chain.
In the Recognition Science foundation layer this sits inside the singular-homology infrastructure that underwrites the eight-tick octave and the circle as the recognition clock (T7). The module doc is explicit that Mathlib still lacks a general simplicial prism/subdivision operator; the equivalence lets either geometric filling strategy discharge the other without reopening the integer-winding side, which is already closed by the directed-cycle kernel theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.