closedSingularOneCycleList_zeroWinding_residual
plain-language theorem explainer
For any finite list of closed singular 1-cycle generators on S¹, there is an integer n equal to the list's total winding such that subtracting n copies of the fundamental cycle leaves a residual of winding zero. Anyone reducing H₁(S¹;ℤ) generation to a zero-winding filling problem cites this. The proof extracts the integer winding, then uses linearity of the winding map and winding(fundamental)=1.
Claim. For every finite list of closed singular one-cycle terms on $S^1$, there exists an integer $n$ such that the winding number of the associated degree-$1$ cycle equals $n$, and the winding of that cycle minus $n$ times the fundamental cycle is zero.
background
This module lifts path-level winding on $S^1$ to singular $1$-simplices and proves that winding kills boundaries, giving a homology invariant. A closed-generator term is a singular $1$-simplex whose two faces agree (so it is a loop) together with an integer coefficient; a finite list of such terms assembles, by summation, into a genuine degree-$1$ cycle in the singular chain complex of $\mathrm{TopCat.sphere},1$ with $\mathbb{Z}$ coefficients.
Cycle winding is the real number obtained by including a $1$-cycle into $C_1(S^1;\mathbb{Z})$ and applying the winding chain map. The fundamental cycle is the once-around generator; upstream work already shows its winding is $1$, and that every finite closed-generator list has integer winding.
The local goal is the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$: winding is a left inverse to the fundamental class. Surjectivity (generation) needs a geometric filling argument still conditional on zero-winding cycles bounding.
proof idea
Term-mode proof. First apply closedSingularOneCycleList_winding_integral to obtain an integer $n$ with winding of the list-cycle equal to $n$. It remains to show the residual after subtracting $n$ times the fundamental cycle has winding zero. Unfold the definition of cycle winding, push the difference through the chain map via map_sub, rewrite the first summand by the chosen $n$, and replace winding of the fundamental multiple by cycleWinding_fundamentalCycle. The resulting real identity $n-n=0$ is discharged by ring.
why it matters
This is the algebraic shell around the remaining geometric filling problem: once zero-winding cycles are known to bound, every closed-generator list is homologous to an integer multiple of the fundamental cycle. The sole downstream consumer is closedSingularOneCycleList_boundary_generates_of_zeroWindingCycles_bound, whose doc-comment states exactly that reduction: choose the list's integer winding, subtract that multiple of the fundamental cycle, and fill the zero-winding residual.
In the broader Recognition chain this supplies the generation half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$, the integer comparison map on the singular complex whose degree-$1$ homology is flagged as the strict T8 target in the circle $H_1$ computation module. It does not itself close T8; it isolates the residual that the prism/subdivision argument must kill.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.