orientedWinding_eq_pathDisplacement
plain-language theorem explainer
For any singular edge equipped with a traversal orientation, its oriented winding equals the path displacement of the corresponding oriented path, divided by 2π. Anyone assembling closed-walk winding sums or the oriented form of H₁(S¹) integrality cites this identity. The proof is a two-case split on orientation: forward is the unoriented equality; backward composes reverse-path displacement with a sign flip.
Claim. Let $o$ be a singular $1$-simplex on $S^1$ together with a traversal orientation. Write $W(o)$ for its oriented winding and $\gamma_o$ for the continuous path on $S^1$ obtained by traversing the edge forward or backward according to the orientation. Then $W(o) = \mathrm{disp}(\gamma_o)/(2\pi)$, where $\mathrm{disp}$ is the endpoint difference of the canonical real lift of the path.
background
This module lifts the path-level winding/displacement invariant of CircleWinding to singular simplices of $S^1$ and proves that winding kills boundaries, giving the injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
Path displacement $\mathrm{disp}(\gamma)$ is the net travel of the canonical lift of a path $\gamma:I\to S^1$ in $\mathbb{R}$. Singular winding of an unoriented edge is that displacement normalized by one full turn $2\pi$. An oriented singular edge pairs a singular $1$-simplex with a forward/backward flag; oriented winding is the singular winding, negated on backward traversal, and the oriented edge path is the corresponding (possibly reversed) continuous path.
The unoriented comparison singularWinding_eq_pathDisplacement already equates singular winding with normalized path displacement. Reversal negates displacement (pathDisplacement_reverse).
proof idea
Destructure the oriented edge into its underlying singular edge and orientation flag, then case on the flag.
Forward: both sides reduce by definition to the unoriented quantities, so the claim is exactly singularWinding_eq_pathDisplacement.
Backward: oriented winding is $-$singular winding and the oriented path is the reverse path. Rewrite the right-hand side with pathDisplacement_reverse (displacement flips sign under reverse) and neg_div, then apply the unoriented equality again.
why it matters
Oriented edges are the atomic summands in closed-walk winding. This identity converts each oriented winding contribution into a normalized path displacement, so cyclic connectivity of oriented terminals/initials becomes path endpoint matching and total winding becomes a telescoping lift difference.
Downstream, orientedWindingSum_cyclic_integral uses it for the oriented closed-walk integrality theorem: a cyclically connected family of oriented edges has integer total oriented winding. The immediate corollary OrientedSingularEdge.singularWinding_terminalReturnSide also rewrites through this equality.
In the module's larger program this supports the covering-space winding homomorphism that is a left inverse to the fundamental class (injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$). Surjectivity/generation remains open pending a simplicial prism or subdivision operator Mathlib does not yet supply. No Recognition forcing-chain step (T0–T8) is invoked here; the result is pure circle topology scaffolding for later RS geometric uses of winding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.