closedSingularOneCycle_boundary_generate_of_zero_winding_coneCirclePoint
plain-language theorem explainer
When a closed singular edge on S¹ has zero winding, its cycle is homologous to zero times the fundamental class: the whole edge is a 2-boundary from the explicit cone. Cite this for the generation half of H₁(S¹;ℤ) ≅ ℤ in the zero-winding single-edge case. The proof is a thin wrapper: take the bounding cone chain and set the fundamental coefficient to 0.
Claim. Let $f:\Delta^1\to S^1$ be continuous with $f(v_1)=f(v_0)$ and simplex winding $0$. Then there exist $n\in\mathbb{Z}$ and a singular $2$-chain $b$ on $S^1$ such that the closed singular $1$-cycle of $f$ equals $\partial b + n\,[S^1]$, where $[S^1]$ is the fundamental cycle. (The construction yields $n=0$.)
background
The module lifts path winding on $S^1$ to singular $1$-simplices. A OneSimplex is a continuous map $f:\Delta^1\to S^1$. The real invariant simplexDisplacement (equivalently $2\pi$ times simplexWinding) is path displacement after reparameterizing $\Delta^1$ to $[0,1]$. The key identity is that alternating face displacements of any singular $2$-simplex vanish, so winding kills boundaries and induces a homology invariant.
Together with the fact that the once-around generator has winding $1$, this gives a left inverse to the fundamental class (injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$). Generation (every $1$-cycle homologous to an integer multiple of the fundamental cycle) needs prism/subdivision constructions Mathlib singular homology does not yet supply in full.
Upstream, closedSingularOneCycle packages a closed singular edge as a degree-$1$ cycle in sphereOneSingularIntChainComplex (Mathlib singular chains on TopCat.sphere 1 with $\mathbb{Z}$ coefficients). The sibling cone theorem produces an explicit $2$-chain whose boundary is that cycle when winding vanishes.
proof idea
One-line generation wrapper around the cone bound. Invoke closedSingularOneCycle_bounds_of_zero_winding_coneCirclePoint on $f$, the equal-endpoint hypothesis, and zero winding to obtain a $2$-chain $b$ with $\partial b$ equal to the closed edge cycle. Instantiate the existential with coefficient $n=0$ and that same $b$. Rewrite the $n$-summand via map_zero, simplify, and finish by symmetry of the cone identity.
why it matters
Generation-shaped packaging of the zero-winding closed-edge cone: the integer coefficient of the fundamental cycle is forced to $0$, and the entire edge is accounted for by an explicit cone boundary. That is exactly the algebraic form needed by consumers that compare an arbitrary closed edge to $n[S^1]$ modulo $2$-boundaries (the doc immediately below describes that consumer pattern).
In the module's program this is a local piece of the surjective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The chain complex is the object whose degree-$1$ homology is the strict foundation target tied to the circle generator (and thence the T8 spatial-dimension forcing chain). No downstream theorems yet depend on this declaration; it sits as the generation-shaped API over the analytic cone bound.
It does not close full generation for arbitrary $1$-cycles; that still needs global prism/subdivision operators beyond single-edge zero winding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.