pathWinding_loop_integral
plain-language theorem explainer
A continuous closed path on the unit circle has integer winding number: the normalized lift displacement equals some k in Z. Topologists and anyone tracking RS circle-covering invariants cite this when converting displacement into a true winding. The proof is a short reduction: take the integer multiple of 2π from the displacement lemma and divide by 2π.
Claim. Let $\gamma : I \to S^1$ be continuous with $\gamma(1) = \gamma(0)$. Then there exists $k \in \mathbb{Z}$ such that the winding number of $\gamma$ equals $k$ as a real number.
background
This module builds the local winding (displacement) invariant for paths in the exact TopCat.sphere 1 carrier, written here as $S^1$. Paths lift through the trigonometric covering map to $\mathbb{R}$; displacement is how far the canonical lift travels. The key upstream fact is that any two continuous lifts of one path that start in the same fiber differ by a constant deck transformation in $2\pi\mathbb{Z}$, so displacement is independent of lift choice.
Winding is displacement normalized by one full turn: $\mathrm{pathWinding}(\gamma) = \mathrm{pathDisplacement}(\gamma)/(2\pi)$. The sibling theorem pathDisplacement_loop_intMul already shows that a closed path has displacement equal to an integer number of full turns: $\mathrm{pathDisplacement}(\gamma) = k \cdot 2\pi$ for some $k \in \mathbb{Z}$. The present result is the normalized form of that statement.
No project-local $S^1$ stand-ins or axioms are used; the covering is Mathlib's trigonometric covering of the exact sphere object.
proof idea
One short tactic proof. Obtain $k$ and the equality $\mathrm{pathDisplacement}(\gamma) = k \cdot 2\pi$ from pathDisplacement_loop_intMul using the closed-path hypothesis. Unfold pathWinding (displacement over $2\pi$), rewrite with that equality, and cancel the nonzero factor $2\pi$ by field_simp after a positivity check. No new covering or uniqueness argument is needed here.
why it matters
Integer winding is the discrete invariant that later chain and ledger constructions need when a continuous loop is treated as a singular 1-simplex. Downstream, simplexWinding_loop_integral in CircleWindingChain applies this theorem after unfolding the simplex-to-path bridge: a singular 1-simplex with agreeing endpoints has integer winding.
In the Recognition foundation layer this sits under the circle-covering infrastructure that supports continuum bridges and ledger displacement. It does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law; it supplies the topological integrality step those continuum identifications rely on when loops close. The module claims zero sorry and no axioms, so this is a closed proved link rather than scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.