zeroWindingCycles_bound_of_fundamentalCycle_boundary_generates
plain-language theorem explainer
If every singular 1-cycle on S¹ is a 2-boundary plus an integer multiple of the fundamental cycle, then every zero-winding 1-cycle is a boundary. Algebraic topologists computing H₁(S¹;ℤ) ≅ ℤ cite this reduction. The proof writes z = ∂b + n·γ, notes winding kills boundaries and sends γ to 1, so W(z)=0 forces n=0.
Claim. Assume every degree-$1$ singular cycle $z$ on $S^1$ decomposes as $z = \partial b + n\cdot\gamma$ for some singular $2$-chain $b$ and integer $n$, where $\gamma$ is the fundamental once-around cycle. Then every $1$-cycle with winding number zero is a boundary: $W(z)=0$ implies $z=\partial b'$ for some $b'$.
background
This module lifts path-level winding on $S^1$ to singular simplices and proves that winding kills boundaries, so it descends to a homology invariant. The winding of a degree-$1$ cycle is obtained by including the cycle into $C_1(S^1;\mathbb{Z})$ and applying the winding chain map; on the fundamental cycle $\gamma$ it returns the integer coefficient (so $W(n\gamma)=n$).
The hypothesis fundamentalCycle_boundary_generates is the concrete chain-level generation statement: every $1$-cycle equals a lifted singular $2$-boundary plus an integer multiple of the lifted fundamental cycle. The conclusion zeroWindingCycles_bound asserts that every zero-winding $1$-cycle is homologous to zero (i.e., bounds).
The ambient complex is Mathlib's singular chain complex of $\mathrm{TopCat.sphere},1$ with integer coefficients, whose degree-$1$ homology is the strict T8 target $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Winding already supplies the split-injective half; generation is the remaining geometric half.
proof idea
Tactic proof, about thirty lines. Fix a $1$-cycle $z$ with $W(z)=0$. Apply the generation hypothesis to obtain $n$ and a $2$-chain $b$ with $z=\partial b+n\cdot\gamma$.
First show the winding of any boundary vanishes: compose toCycles with the winding chain map and rewrite by windingChainMap_boundary, then simplify. Next compute $W(z)$ by additivity: $W(z)=W(\partial b)+W(n\gamma)=0+n$, using cycleWinding_fundamentalCycle. The hypothesis $W(z)=0$ therefore forces $n=0$ over $\mathbb{R}$, hence $n=0$ in $\mathbb{Z}$ by exact_mod_cast. Substitute back to conclude $z=\partial b$.
why it matters
This is the clean algebraic reduction that isolates all remaining geometric work into one Prop: prove chain-level generation by the fundamental cycle, and zero-winding filling follows for free. Downstream, the iff theorem equates the two formulations once integer-valued winding is in hand. Two concrete generation routes also land here: one-directed-cycle terms and oriented cyclic families each reduce to this implication after a short preprocessing lemma.
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 the circle generator). Winding already gives the left inverse to the fundamental class; this lemma packages the converse half so that any future prism/subdivision construction only needs to discharge fundamentalCycle_boundary_generates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.