singularTwoBoundaryFree_freeMk_coneCircleMap_of_simplexWinding_zero
plain-language theorem explainer
Zero-winding specialization of the cone boundary identity on singular chains of the circle. If a singular 1-simplex has winding number zero, the free boundary of its cone 2-simplex equals the free generator of that edge alone. Anyone building the winding map on H₁(S¹;ℤ) would cite it. Proof rewrites the general cone boundary shell, collapses the terminal-return face by the zero-winding lemma, then cancels with abel.
Claim. Let $f:\Delta^1\to S^1$ be a continuous singular $1$-simplex with winding number zero. Write $\mathrm{Cone}(f)$ for the singular $2$-simplex obtained by coning the path of $f$ to its initial point (with the standard continuous cone map). Then the free singular boundary sends the free generator of $\mathrm{Cone}(f)$ to the free generator of $f$: $$\partial^{\mathrm{free}}([\mathrm{Cone}(f)])=[f].$$
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, the chain-level fact needed for a homology invariant. A singular $1$-simplex is a continuous map $f:\Delta^1\to S^1$; simplexWinding is the integer winding obtained by reparameterizing $\Delta^1$ to the unit interval and taking path winding. The cone construction packages a continuous pointwise cone of a unit-interval path to its initial point as a singular $2$-simplex of $S^1$.
The free boundary map is the induced map on free $\mathbb{Z}$-modules generated by singular simplices (the singular chain boundary, written here via ModuleCat). In the unrestricted cone boundary identity, three faces appear: the base edge, a terminal-return side, and a constant apex side. Upstream, the zero-winding lemma states that when winding vanishes, the terminal-return side equals the constant apex edge at the path's initial point, because the path lift closes and the two endpoint lifts agree.
proof idea
Term-mode proof in three steps. First rewrite by the general identity singularTwoBoundaryFree_freeMk_coneCircleMap, which expands the free boundary of any continuous cone $2$-simplex into an alternating combination of base, terminal-return, and constant faces in the free module. Second, invoke coneTerminalSide_eq_constantOneSimplex_of_simplexWinding_zero on $f$ and the winding-zero hypothesis to replace the terminal-return face by the constant apex $1$-simplex at the initial point of the path of $f$. Third, abel cancels the two identical constant faces against each other in the free abelian group, leaving only the free generator of the original edge $f$.
why it matters
Sits in the Foundation circle-winding chain that supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$: winding on $1$-cycles is a left inverse to the fundamental class, once boundaries are known to have winding zero. The module doc frames the parent goal as the kills-boundaries identity plus the once-around generator evaluation; this lemma is the zero-winding specialization of the cone boundary shell that makes the free boundary of a null-homologous cone collapse cleanly to the original edge. No downstream uses are recorded yet. It does not touch the generation/surjectivity half (every $1$-cycle homologous to an integer multiple of the fundamental cycle), which the module notes still needs a simplicial prism or subdivision operator absent from Mathlib singular homology. No direct link to the T0–T8 forcing chain or RCL; pure topological foundation for circle homology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.