simplexWinding
plain-language theorem explainer
Normalised winding number of a singular 1-simplex on S¹: angular displacement divided by 2π. Anyone citing the chain-level winding homomorphism, zero-winding cone fillers, or the split-injective half of H₁(S¹;ℤ) ≅ ℤ uses this scalar. The body is a one-line normalisation of the already-defined simplex displacement.
Claim. For a continuous map $f : \Delta^1 \to S^1$, the winding number is $\mathrm{wind}(f) := \mathrm{disp}(f)/(2\pi)$, where $\mathrm{disp}(f)$ is the lift-independent angular travel of the path obtained by reparameterising $f$ along the unit interval.
background
The module lifts the path-level winding/displacement invariant from CircleWinding to singular simplices of $S^1$, and proves that displacement kills boundaries. A singular 1-simplex is a continuous map $f : \Delta^1 \to S^1$ with $\Delta^1 = \mathrm{stdSimplex},\mathbb{R},(\mathrm{Fin},2)$. Reparameterising $\Delta^1$ to $[0,1]$ yields a path; path displacement is the net angular travel of any continuous lift to $\mathbb{R}$, independent of the choice of lift.
Simplex displacement is exactly that path displacement. Dividing by $2\pi$ converts radians of travel into an integer-valued winding count on closed loops (and a real-valued count in general). The companion fact is that the alternating face sum of displacements on any singular 2-simplex vanishes, so the invariant descends to homology.
proof idea
Pure definitional wrapper: evaluate simplex displacement of $f$, then divide by $2\pi$. No tactics, no lemmas beyond the already-constructed displacement of the reparameterised path.
why it matters
This is the scalar that the rest of the CircleWindingChain module treats as the chain-level winding homomorphism. Downstream theorems use vanishing of this quantity as the hypothesis that a closed singular edge bounds: the zero-winding cone fillers, side-face equalities of the continuous cone, collapse of the terminal-return side to a constant edge, and the generation-shaped form that writes the edge as an explicit cone boundary with fundamental-cycle coefficient 0.
Together with the fact that the once-around generator has winding 1, it supplies the left-inverse half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The module notes that the converse (every 1-cycle homologous to an integer multiple of the fundamental cycle) still needs a simplicial prism/subdivision operator not yet in Mathlib singular homology. In the Recognition foundation stack this is the concrete integer invariant that makes the circle's first homology split-injective before any physics constants are introduced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.