closedSingularOneCycle_bounds_of_zero_winding_coneCirclePoint
plain-language theorem explainer
A closed continuous map from the standard 1-simplex into the circle with vanishing simplex winding is a boundary in the integer singular chain complex of S¹. Anyone showing that zero-winding closed edges are homologous to zero will cite this. The proof is a one-line wrapper: it applies the cone-filler theorem and discharges the remaining continuity hypothesis via the continuous cone on the reparameterized path.
Claim. Let $f:\Delta^1\to S^1$ be continuous. If $f(v_1)=f(v_0)$ and the simplex winding of $f$ vanishes, then the closed singular $1$-cycle generated by $f$ is a boundary: there exists an integer singular $2$-chain $b$ on $S^1$ with $\partial b$ equal to that cycle.
background
This module lifts the path-level winding/displacement invariant of the circle to singular simplices of $S^1$, and proves that winding kills boundaries. A singular $1$-simplex is a continuous map $f:\Delta^1\to S^1$ from the standard topological $1$-simplex. The quantity simplexWinding is the integer winding obtained by reparameterizing $\Delta^1$ to the unit interval and taking path winding; closedness means the two endpoints of $f$ agree on $S^1$.
The ambient chain object is Mathlib's singular chain complex of $\mathrm{TopCat.sphere},1$ with integer coefficients. From a closed singular edge one builds an actual cycle element via the lift-to-cycles map. The upstream cone theorem already produces a bounding $2$-chain once the explicit cone map over the lifted path is known to be continuous; that continuity is the last analytic hypothesis on the single-edge construction.
Together with the kills-boundaries identity for $2$-simplices and the fact that winding sends the once-around generator to $1$, this feeds the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
proof idea
One-line term wrapper. It applies the continuity-hypothesis form of the closed-edge cone filler, which already builds the singular $2$-chain whose boundary is the closed cycle once Continuous (coneCirclePoint (oneSimplexPath f)) is supplied. That continuity obligation is discharged by the lemma that the cone over the path associated to $f$ is continuous. Endpoints-closed and zero simplex winding are passed through unchanged.
why it matters
Removes the last analytic hypothesis from the single-edge zero-winding cone construction, so consumers no longer carry a bare continuity side-condition. Downstream it feeds the generation-shaped form (the integer coefficient of the fundamental cycle is $0$; the whole edge is accounted for by the explicit cone boundary) and the actual-singular-simplex form (any closed Mathlib singular $1$-simplex with zero singular winding bounds).
In the module's program this is a brick toward the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$: winding is a left inverse to the fundamental class. The chain complex itself is the exact object whose degree-$1$ homology is the strict T8 target in the forcing chain. The converse generation half (every $1$-cycle homologous to an integer multiple of the fundamental cycle) still needs a simplicial prism/subdivision operator that Mathlib singular homology does not yet supply.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.