closedSingularOneCycle_bounds_of_continuous_coneCirclePoint
plain-language theorem explainer
A closed singular 1-simplex on S¹ with vanishing winding is a singular boundary once the explicit cone over its path lift is continuous. Cite this when discharging zero-winding edges in the integer singular chain complex of the circle. The proof is a short term application of the closed-cone bounding lemma, inserting the continuous cone map and its face identities.
Claim. Let $f:\Delta^1\to S^1$ be a continuous singular $1$-simplex with equal endpoints and simplex winding number zero. If the cone map associated to the path reparameterization of $f$ is continuous, then the integer singular $1$-cycle generated by $f$ is a boundary: there exists a degree-$2$ singular chain $b$ such that $\partial b$ equals that cycle in the singular chain complex of $S^1$ with coefficients in $\mathbb{Z}$.
background
This module lifts the path-level winding/displacement invariant of CircleWinding 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$; its simplex winding is the path winding of the unit-interval reparameterization. Closed means the two vertices of $\Delta^1$ land on the same point of $S^1$, so $f$ defines a singular $1$-cycle via the standard lift-to-cycles map.
The ambient complex is Mathlib's singular chain complex of $\mathrm{TopCat.sphere},1$ with integer coefficients; its degree-$1$ homology is the strict T8 target $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The cone construction fills a closed edge by coning the lifted path in the covering line and projecting back to the circle; continuity of that cone is the remaining analytic input after all combinatorial face identities are in place.
Upstream, the closed-cone bounding lemma already shows that any singular $2$-simplex whose faces match the closed edge (and whose side faces cancel under zero winding) witnesses the boundary relation in the chain complex.
proof idea
Term-mode one-shot wrapper. Apply the closed-cone bounding lemma to $f$ and the endpoint hypothesis, supplying three data:
- the singular $2$-map built from continuity of the cone point map on the path of $f$;
- the face-$2$ identity for that continuous cone map;
- the side-face cancellation identity, which uses zero winding together with continuity.
No extra tactics: the four arguments match the general lemma's hypotheses exactly, and the existential $2$-chain is returned as the image of that cone under the singular chains functor.
why it matters
Parent theorem is the zero-winding cone form that drops the continuity hypothesis from the user-facing statement: "A closed singular edge with zero winding bounds by the explicit continuous cone over its lifted path. This removes the last analytic hypothesis from the single-edge zero-winding cone construction."
Together with the kills-boundaries identity (simplexDisplacement_boundary) and the fact that winding sends the once-around generator to $1$, this supplies the generation direction for zero-winding edges in the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. That isomorphism is the chain-level landmark feeding the strict T8 computation (three spatial dimensions via the eight-tick octave and circle homology).
The full surjectivity half still needs a simplicial prism/subdivision operator that Mathlib's singular homology does not yet provide; this lemma closes only the single-edge continuous-cone case.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.