singularEdgePath_homotopicRel_const_of_loop_winding_zero
plain-language theorem explainer
A closed singular 1-simplex on the circle with vanishing singular winding is path-homotopic, relative to endpoints, to the constant path at its basepoint. Anyone assembling the singular prism or proving that zero-winding closed edges bound will cite this. The argument is a short reduction to the path-level null-homotopy theorem: face equality becomes loop closure, and singular winding is identified with path winding.
Claim. Let $s$ be a singular $1$-simplex on $S^1$. If the two $0$-faces of $s$ coincide (so the edge is closed) and the singular winding number of $s$ equals $0$, then the continuous path associated to $s$ is homotopic relative to $\{0,1\}$ to the constant path at its initial point.
background
This module lifts the path-level winding and displacement invariant of the circle to singular simplices of $\mathrm{TopCat.sphere},1$, and proves that winding kills boundaries. A singular $1$-simplex is a continuous map $\Delta^1\to S^1$ in the singular simplicial set; reparameterizing $\Delta^1$ to the unit interval $I$ yields an ordinary path, whose displacement (normalized by $2\pi$) is the singular winding.
At path level, winding is homotopy-invariant and additive under concatenation. The key upstream fact is that a closed path $\gamma:I\to S^1$ with $\mathrm{pathWinding}(\gamma)=0$ is homotopic rel endpoints to the constant path at $\gamma(0)$: the covering lift to $\mathbb{R}$ has matching endpoints, contracts linearly, and projects back. The present statement is the same claim written for a singular edge whose $0$-faces agree.
Together with the kills-boundaries identity on $2$-simplices and the fact that the fundamental loop has winding $1$, this feeds the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
proof idea
One-line reduction to the path-level theorem pathHomotopicRel_const_of_loop_winding_zero.
First goal: the singular edge path is a loop. Rewrite its values at $0$ and $1$ via the endpoint lemmas for the edge path, then push the given face equality through the vertex-point map so the path endpoints match.
Second goal: path winding vanishes. Unfold path winding, rewrite via the identity equating singular winding to path displacement (normalized), and apply the hypothesis that singular winding is zero.
No covering-space work is redone here; that lives entirely in the upstream path theorem.
why it matters
This is the path-level null-homotopy input required by the remaining singular prism construction on the circle. Downstream it is used by closedSingularOneCycle_bounds_of_raw_boundary: a raw singular $2$-chain whose boundary is the raw generator of a closed singular edge already proves that the closed generator cycle bounds. That is the raw-chain form of the free-boundary bounding statement for closed singular one-cycles.
In the module narrative, winding on singular $1$-simplices plus the kills-boundaries identity give a left inverse to the fundamental class (injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$). Surjectivity still needs a simplicial prism or subdivision operator that Mathlib singular homology does not yet supply; this lemma is a necessary path-homotopy brick for that generation half, without introducing project-local $S^1$ replacements or axioms.
It sits in the Foundation layer that underwrites topological invariants used later in the Recognition forcing chain, but it is pure circle topology: no appeal to $J$-cost, $\varphi$, or the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.