singularWinding_coneTerminalSide
plain-language theorem explainer
For any continuous path γ on S¹, the singular winding of the Mathlib singular 1-simplex obtained from the cone's terminal-return side equals the negative of the path's displacement divided by 2π. Anyone tracking the cone construction that witnesses winding annihilating boundaries will cite this. The proof is a two-line rewrite through the map-to-singular bridge and the already-proved simplex-level identity.
Claim. For every continuous path $\gamma : I \to S^1$, the singular winding number of the singular $1$-simplex associated to the cone terminal-return side of $\gamma$ equals $-\frac{\mathrm{disp}(\gamma)}{2\pi}$, where $\mathrm{disp}(\gamma)$ is the endpoint difference of the canonical real lift of $\gamma$.
background
This module lifts the path-level displacement/winding invariant of CircleWinding to singular simplices of Mathlib's TopCat.sphere 1, and proves that winding annihilates boundaries: $W \circ \partial_2 = 0$. Displacement of a path $\gamma$ is $\mathrm{pathLift},\gamma,1 - \mathrm{pathLift},\gamma,0$, the net travel of the canonical lift in $\mathbb{R}$. Winding is that quantity divided by $2\pi$.
The cone over $\gamma$ supplies a singular $2$-simplex whose faces relate the base path to a terminal-return side. The terminal-return side is the concrete continuous $1$-simplex that runs the reverse of the lifted path on the standard $\Delta^1$, then projects by the trigonometric covering. singularOneSimplexOfMap packages such a continuous map into Mathlib's singular simplicial set.
Upstream, simplexWinding_coneTerminalSide already states the same numerical identity at the concrete-simplex level: the terminal-return side has winding opposite the base displacement. The present theorem is the singular-set packaging of that fact.
proof idea
One-line (two-rewrite) wrapper. First apply singularWinding_singularOneSimplexOfMap, which identifies singular winding of the packaged singular simplex with ordinary simplex winding of the underlying continuous map. Then apply simplexWinding_coneTerminalSide, which unfolds simplex winding to displacement, uses the cone-terminal path-displacement identity, and finishes by ring arithmetic to obtain $-(\mathrm{disp}(\gamma)/(2\pi))$.
why it matters
The cone faces are the generators used to check that the winding cochain kills singular boundaries. Downstream, OrientedSingularEdge packages a singular edge with a traversal orientation; this identity fixes the signed winding contribution of the terminal-return face under that orientation.
In the module's larger program, winding on $1$-cycles plus pathWinding_fundamentalLoop (generator maps to $1$) gives the split-injective half of $H_1(S^1;\mathbb{Z}) \cong \mathbb{Z}$. The cone telescoping that proves $W \circ \partial_2 = 0$ needs consistent signs on all three faces; this theorem locks the terminal-return sign at the actual singular-set level, not merely the concrete $C(\Delta^1,S^1)$ level.
No Recognition forcing-chain landmark (T5–T8, RCL, $\varphi$) is invoked here: the result is pure circle topology supporting the foundation homology computation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.