closedSingularOneCycleList_bounds_of_forall_zero_singularWinding
plain-language theorem explainer
Any finite list of closed singular 1-simplices on the circle with vanishing winding represents a boundary in the integer singular chain complex of S¹. Workers assembling the injective half of H₁(S¹;ℤ) ≅ ℤ cite this when collapsing zero-winding generator sums to a single 2-chain. The argument is list induction: the empty sum bounds by zero; the cons case adds the single-term cone witness to the inductive tail witness.
Claim. For every finite list of closed-generator terms on $S^1$, if each term has singular winding zero, then the integer singular $1$-cycle obtained by summing those terms equals the image of some singular $2$-chain under the degree-$(2\to 1)$ cycles map of the singular chain complex of $S^1$ with coefficients in $\mathbb{Z}$.
background
The module lifts the path-level winding invariant of the circle to singular simplices of $\mathrm{TopCat.sphere},1$ and proves that winding kills boundaries. A singular $1$-simplex gets a real displacement (equivalently $2\pi$ times winding) by reparameterizing $\Delta^1$ to the unit interval; the key identity is that the alternating face sum of displacements on any singular $2$-simplex vanishes, by convexity of $\Delta^2$ plus path-displacement additivity and homotopy invariance.
A closed-generator term packages one singular $1$-simplex whose two faces agree (so it is a loop), together with an integer coefficient. The list construction sums those terms into a degree-$1$ cycle of the Mathlib singular chain complex of $S^1$ with $\mathbb{Z}$ coefficients. Singular winding is the integer winding of that simplex; the single-term cone construction already produces a bounding $2$-chain whenever that winding is zero. This declaration is the finite-sum consumer of those cone witnesses.
proof idea
Proof by induction on the list of terms.
Empty list: take the zero $2$-chain; unfolding the list-cycle definition and simplifying shows the empty sum is the image of zero under the cycles map.
Cons case: the universal zero-winding hypothesis specializes to the head and to the tail. The head supplies a single-term cone witness via the existing zero-winding bound for one closed-generator term. The inductive hypothesis supplies a $2$-chain for the tail. Their sum is the required witness: unfolding the list-cycle definition, rewriting by the two equalities, and applying additivity of the cycles map finishes the step.
why it matters
Doc-comment places this as the first finite-sum consumer of the cone construction for zero-winding closed generators. Together with the single-simplex kills-boundaries identity and the fact that the once-around loop has winding one, it supports the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$: winding is a homology invariant that left-inverts the fundamental class.
In the Recognition foundation stack this is chain-level infrastructure for the circle's first homology, the same object whose degree-$1$ homology is flagged as the strict T8 target in the singular-complex abbreviation. Surjectivity (every $1$-cycle homologous to an integer multiple of the fundamental cycle) remains the open generation half and needs a prism or subdivision operator Mathlib does not yet supply. No downstream consumers are wired yet; the lemma closes the finite-sum gap so those consumers can treat arbitrary zero-winding generator lists as boundaries.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.