closedSingularOneCycle_bounds_of_closed_cone_map
plain-language theorem explainer
Endpoint-form cone criterion for closed singular 1-cycles on S¹: a continuous closed edge bounds in singular homology once a continuous 2-simplex exists with that edge as base and equal side faces. Cited by anyone discharging zero-winding nullhomotopies at chain level. One-line handoff to the face-form cone theorem after converting endpoint agreement into face equality.
Claim. Let $f:\Delta^1\to S^1$ be continuous with $f(v_1)=f(v_0)$. If there is a continuous $F:\Delta^2\to S^1$ whose base face equals $f$ and whose two lateral faces agree, then the integer singular $1$-cycle generated by $f$ is a boundary in the singular chain complex of $S^1$.
background
This module lifts path-level winding on $S^1$ to singular simplices and proves that displacement kills boundaries, the chain-level fact needed for a winding homomorphism on $H_1(S^1;\mathbb{Z})$. A OneSimplex is a continuous map $\Delta^1\to S^1$; a TwoSimplex is a continuous map $\Delta^2\to S^1$. Faces of a $2$-simplex are the three edge restrictions.
The object closedSingularOneCycle packages a closed singular $1$-simplex (equal $0$-faces) as an actual degree-$1$ cycle in Mathlib's integer singular chain complex of TopCat.sphere 1. The upstream face-form theorem already says: if a continuous $F$ has base face $f$ and equal side faces, then after transport through the singular simplicial set the corresponding generator bounds. Endpoint agreement on $f$ is the concrete closed-loop condition used by path winding; it implies the two $0$-faces of the singular $1$-simplex agree.
proof idea
One-line term wrapper. Convert the endpoint hypothesis $f(v_1)=f(v_0)$ into equality of the two singular $0$-faces via singularOneSimplexOfMap_faces_eq_of_endpoints, then apply the upstream face-form theorem closedSingularOneCycle_bounds_of_cone_map with the same $F$, base-face identity, and side-face identity. No new chain algebra is performed here.
why it matters
This is the exact handoff left by the zero-winding nullhomotopy program: after path-level winding vanishes, one only needs a conical continuous filler $F:C(\Delta^2,S^1)$ with prescribed base and equal sides. Downstream, closedSingularOneCycle_bounds_of_continuous_coneCirclePoint specializes further to the analytic remaining obligation Continuous (coneCirclePoint (oneSimplexPath f)).
In the module narrative this supports the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$: winding is a left inverse to the fundamental class. That computation is the strict T8-adjacent singular-homology target for the circle (the chain complex is explicitly the object whose degree-$1$ homology is that target). Surjectivity still needs prism/subdivision operators Mathlib does not yet supply.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.