orientedWinding
plain-language theorem explainer
Oriented winding assigns a signed real winding number to a singular 1-edge with a traversal direction: the ordinary singular winding when the edge is taken forward, and its negative when taken backward. Anyone assembling closed oriented walks or cyclic families on S¹ cites this as the edge contribution. The definition is a two-branch match on orientation, with no further proof obligations.
Claim. Given an oriented singular edge $o$ (a singular $1$-simplex of $S^1$ together with a forward or backward traversal flag), the oriented winding of $o$ is the singular winding of the underlying edge if the orientation is forward, and the negative of that winding if the orientation is backward.
background
The module lifts the path-level winding/displacement invariant of the circle to singular simplices of $S^1$, and proves that winding kills boundaries: the alternating face sum of displacements on any singular $2$-simplex vanishes. That identity, with the fact that the once-around generator has winding $1$, yields a winding homomorphism on $1$-cycles that is a left inverse to the fundamental class (the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$).
An oriented singular edge is a singular $1$-simplex paired with an EdgeOrientation (forward or backward). Singular winding is the winding number of a concrete singular $1$-simplex of $\mathrm{TopCat.sphere},1$, obtained by transporting into the singular simplicial set and applying simplex winding (itself path displacement reparameterized from $\Delta^1$ to the unit interval, scaled by $2\pi$).
Oriented winding is the signed version of that number needed when edges appear in closed walks with prescribed traversal direction.
proof idea
Pure definition by cases on the orientation field. Forward returns the singular winding of the underlying edge; backward returns its additive inverse. No lemmas are applied; the body is a match expression.
why it matters
Signed edge contributions are the atomic summands of oriented cyclic families: a finite sign-oriented closed walk in singular $1$-simplices is a family of oriented edges with matching terminal/initial vertices under cyclic rotation. Oriented winding feeds those structures and the comparison lemma equating oriented winding to path displacement of the oriented edge path.
In the broader Recognition foundation story this sits inside the chain-level construction of the winding homomorphism on $H_1(S^1)$, the topological half of identifying the circle's first homology with $\mathbb{Z}$. The module notes that the converse generation half (every $1$-cycle homologous to an integer multiple of the fundamental cycle) still needs a simplicial prism/subdivision operator that Mathlib singular homology does not yet supply; this definition does not close that gap, but it is the signed edge measure those cycle sums use.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.