closedSingularOneCycleList_boundary_generates_of_zeroWindingCycles_bound
plain-language theorem explainer
Under the hypothesis that every zero-winding singular 1-cycle on S¹ is a boundary, any finite closed-generator list equals an integer multiple of the fundamental cycle plus a boundary. Homology workers proving the generation half of H₁(S¹;ℤ) ≅ ℤ cite this. The proof peels off the list winding, fills the residual via the hypothesis, and reassembles with the residual-bound lemma.
Claim. Assume every zero-winding singular $1$-cycle on $S^1$ bounds. Then for every finite list of closed-generator terms, there exist $n \in \mathbb{Z}$ and a singular $2$-chain $b$ such that the cycle of the list equals $\partial b + n\,[S^1]$, where $[S^1]$ is the fundamental singular $1$-cycle.
background
The 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 alternating face displacements of any singular $2$-simplex vanish, so winding is a homology invariant and a left inverse to the fundamental class: the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
A closed-generator term is a singular $1$-simplex whose two faces agree, together with an integer coefficient; a finite list of such terms assembles to a $1$-cycle in the integer singular chain complex of $S^1$. The fundamental cycle is the once-around generator. The residual after subtracting the list's total winding times that generator is a zero-winding cycle.
Upstream, the residual-bound lemma already says: if that residual is a boundary, the original list is homologous to an integer multiple of the fundamental cycle. The present result packages the global filling hypothesis for all zero-winding cycles with that residual construction.
proof idea
Term-mode, three steps. First apply the zero-winding residual lemma to the list: obtain an integer $n$ so that list-cycle minus $n$ times the fundamental cycle is a zero-winding residual. Second, feed that residual to the hypothesis that zero-winding cycles bound, producing a $2$-chain $b$ with $\partial b$ equal to the residual. Third, invoke the residual-bound generation lemma on $(ts,n,b)$ to reassemble the equality list-cycle $= \partial b + n,[S^1]$.
why it matters
This is the filling half of the generation argument for $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Downstream, fundamentalCycle_boundary_generates_of_closedSingularOneCycleList_spans combines it with a finite-support spanning hypothesis: every $1$-cycle is homologous to some closed-generator list, and under zero-winding filling the list is homologous to an integer multiple of the fundamental cycle. The module doc states that Mathlib still lacks the simplicial prism/subdivision operator needed for unrestricted generation; this theorem isolates the remaining work into two named interfaces (list spanning and zero-winding filling).
In the Recognition forcing chain the degree-$1$ homology of $S^1$ is the strict T8 target (three spatial dimensions via the eight-tick octave and circle topology). Establishing that the integer comparison map is surjective, not only split-injective via winding, closes the algebraic half of that identification. The declaration itself is fully proved; it only conditions on the zero-winding bound interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.