closedSingularOneCycle_zsmul_bounds_of_zero_singularWinding
plain-language theorem explainer
Any integer multiple of a closed singular 1-simplex of winding zero is a boundary in the integer singular chain complex of S¹. Homology workers computing H₁(S¹;ℤ) cite this when extending the unit cone theorem to free ℤ-coefficients. The proof scales the unit bounding 2-chain by n via ℤ-linearity of the cycle map.
Claim. Let $s$ be a singular $1$-simplex on $S^1$ whose two faces agree (so $s$ is closed) and whose singular winding vanishes. Then for every integer coefficient $n\in\mathbb{Z}$, the degree-$1$ cycle obtained by evaluating the closed-generator cycle map of $s$ at $n$ is a boundary: there exists a singular $2$-chain $b$ with $\partial b$ equal to that cycle.
background
This module lifts the path-level winding/displacement invariant of the circle to singular simplices of TopCat.sphere 1, and proves that winding kills boundaries. A singular $1$-simplex is an element of the singular simplicial set of $S^1$ in degree $1$. Closedness means the two face maps $\delta_0 s=\delta_1 s$, so the alternating boundary vanishes and the simplex defines a $1$-cycle.
The integer singular chain complex of $S^1$ is Mathlib's singularChainComplexFunctor applied to $S^1$ with coefficients in $\mathbb{Z}$. The closed-generator cycle map sends the unit $1\in\mathbb{Z}$ to the cycle carried by a closed singular $1$-simplex. The upstream unit theorem states that any such closed simplex of singular winding zero bounds: there is a $2$-chain whose boundary is that cycle. The present result is the scalar extension of that cone statement to arbitrary free coefficients $n\in\mathbb{Z}$.
proof idea
One-step scalar extension of the unit cone theorem. Apply closedSingularOneCycle_bounds_of_zero_singularWinding to obtain a bounding $2$-chain $b$ for the unit coefficient. Take the candidate $n\bullet b$. ℤ-linearity of the cycle Hom (map_zsmul) gives $\partial(n\bullet b)=n\bullet\partial b$. A short linearity identity rewrites the left-hand side (the closed-generator cycle evaluated at $n$) as $n$ times the same cycle at $1$, which matches $n\bullet\partial b$ by the unit case. The rewrite closes.
why it matters
This is the free-coefficient form of the zero-winding cone on closed singular generators. Downstream it feeds ClosedSingularOneCycleTerm, the single finite-sum term in a closed-generator decomposition of a cycle (simplex, face-equality witness, and integer coefficient). Without the scalar form, only the unit generator would be known to bound; arbitrary free summands in a cycle decomposition would not.
In the module's larger program this supports the generation half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$: every $1$-cycle should be homologous to an integer multiple of the fundamental cycle. The winding homomorphism already supplies the split-injective half (via the kills-boundaries identity and the once-around generator). The remaining gap is building raw prisms/subdivisions so every cycle decomposes into closed generators; this lemma clears the free-coefficient bookkeeping once those generators appear. It is foundation infrastructure for the strict T8 target on the singular homology of $S^1$, not a physics constant claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.