simplexWinding_boundary
plain-language theorem explainer
The alternating sum of winding numbers on the three faces of any singular 2-simplex of the circle vanishes. Homology theorists building the winding map on H₁(S¹) cite this as the chain-level kills-boundaries identity in winding form. The proof is a one-line scaling of the corresponding displacement identity by 1/(2π).
Claim. For every continuous map $F:\Delta^2\to S^1$ from the standard topological $2$-simplex, writing $w$ for the winding number of a singular $1$-simplex (displacement divided by $2\pi$), one has $w(\partial_0 F)-w(\partial_1 F)+w(\partial_2 F)=0$.
background
This module lifts the path-level winding and displacement invariant of the circle to singular simplices of $S^1$, and proves the single identity that makes the invariant a homology class: it kills boundaries.
A singular $2$-simplex is a continuous map $F:\Delta^2\to S^1$, with $\Delta^2=\mathrm{stdSimplex},\mathbb{R},(\mathrm{Fin},3)$. Its three faces are the edge restrictions obtained by composing with the standard face maps. Displacement of a singular $1$-simplex is the real lift difference after reparameterising $\Delta^1$ onto the unit interval; winding is that displacement divided by $2\pi$.
Upstream, the displacement form of the same identity is already proved: the broken boundary walk $v_0\to v_1\to v_2$ inside the convex (hence simply connected) standard $2$-simplex is homotopic rel endpoints to the direct edge $v_0\to v_2$; pushing the homotopy through $F$ and using additivity plus homotopy invariance of path displacement yields vanishing of the alternating face sum.
proof idea
Unfold winding as displacement over $2\pi$. Invoke the already-proved displacement boundary identity on the same $F$. Scale that real equality by $1/(2\pi)$ with linear_combination; the three face terms become the three winding numbers and the right-hand side stays zero. Purely algebraic reduction; no new topology.
why it matters
This is the winding-normalised form of the kills-boundaries identity. Downstream, the singular-set version applies it after transporting from the concrete $2$-simplex presentation to Mathlib's singular simplicial set of the circle, giving $W\circ\partial_2=0$ on generators: the winding cochain annihilates boundaries.
Together with the fact that the invariant sends the once-around generator to $1$, this supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The module notes that the generation half (every $1$-cycle homologous to an integer multiple of the fundamental cycle) still needs a simplicial prism or subdivision operator not yet in Mathlib. In the Recognition foundation stack the result underwrites the topological side of the circle's fundamental class that later feeds octave and forcing constructions (eight-tick period $2^3$).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.