simplexWinding_coneTerminalSide
plain-language theorem explainer
The terminal-return face of the cone over a continuous path on the circle has winding equal to the negative of that path's normalized angular displacement. Anyone evaluating singular winding on cone boundaries cites this identity. The argument unfolds the simplex winding definition, rewrites by the path-level opposite-displacement lemma for the same face, and finishes by ring.
Claim. For every continuous path $\gamma:I\to S^1$, the winding number of the singular $1$-simplex given by the terminal-return side of the cone on $\gamma$ equals $-\mathrm{disp}(\gamma)/(2\pi)$, where $\mathrm{disp}$ denotes the lift-independent angular displacement of $\gamma$.
background
This module lifts the path-level winding/displacement invariant on $S^1$ to singular $1$-simplices and proves the chain-level fact that displacement kills boundaries, supplying the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
A singular $1$-simplex is a continuous map $\Delta^1\to S^1$. Its displacement is the path displacement of the standard reparameterization to the unit interval: the endpoint difference of any continuous lift to $\mathbb{R}$ (independent of the choice of lift up to the deck group $2\pi\mathbb{Z}$). Winding is that real number divided by one full turn $2\pi$.
The cone over a path $\gamma$ has a concrete terminal-return side: the $1$-simplex whose covering coordinate runs linearly from the lifted endpoint of $\gamma$ back to the start. Upstream, the path displacement of that side equals $-\mathrm{disp}(\gamma)$.
proof idea
Short algebraic reduction. Unfold simplex winding and simplex displacement (winding is displacement over $2\pi$; displacement is path displacement of the interval reparameterization of the $1$-simplex). Rewrite via the lemma that path displacement of the terminal-return side equals the negative of the base path's displacement. Finish with ring to rearrange the sign and the $2\pi$ normalization.
why it matters
Direct input to the singular-level companion, which packages the same cone face as a singular $1$-simplex and records the identical opposite-winding identity. That companion sits inside the free-boundary shell for the cone over an arbitrary singular edge: the boundary is the terminal-return side minus the constant apex side plus the original edge. The zero-winding loop theorem is the special case in which the terminal-return side coincides with the constant side.
Together with the $2$-simplex telescoping identity (alternating face displacements sum to zero) and the fact that the once-around generator has winding $1$, this supports the winding homomorphism as a left inverse to the fundamental class. Surjectivity of the integer comparison map (every $1$-cycle homologous to an integer multiple of the fundamental cycle) remains open, pending a simplicial prism/subdivision operator not yet supplied by Mathlib.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.