pathDisplacement_loop_intMul
plain-language theorem explainer
A continuous loop on the exact unit circle has real displacement equal to an integer multiple of $2\pi$. Anyone computing the local winding invariant from the trigonometric covering cites this. The argument lifts the path, matches endpoints in the fiber, and reads off the deck group $2\pi\mathbb{Z}$.
Claim. Let $\gamma : I \to S^1$ be continuous with $\gamma(1)=\gamma(0)$. Then there exists $k\in\mathbb{Z}$ such that the path displacement of $\gamma$ equals $k\cdot 2\pi$.
background
This module builds a local winding (displacement) invariant for paths in the exact TopCat.sphere 1 carrier, written $S^1$ here. The covering map is the trigonometric parametrization sending a real angle $t$ to the corresponding point of $S^1$. A path $\gamma:I\to S^1$ is lifted canonically to a continuous real path whose start sits in the chosen fiber; displacement is the endpoint difference of that lift.
The fiber law is the deck group of the universal cover: two reals map to the same circle point exactly when they differ by an integer multiple of $2\pi$. Lift independence (the module's central technical fact) says the same displacement is recovered from any continuous lift, so later arguments may choose convenient lifts.
The present statement specializes to closed paths: endpoints of $\gamma$ agree, so the lifted endpoints lie in one fiber and their difference is forced into $2\pi\mathbb{Z}$.
proof idea
Because the canonical lift projects to $\gamma$, the images of its endpoints under the covering equal $\gamma(1)$ and $\gamma(0)$. The loop hypothesis identifies those, so the lifted endpoints share a fiber. The fiber characterization then supplies an integer $k$ with lifted end equal to lifted start plus $k\cdot 2\pi$. Displacement is defined as that endpoint difference, and a short algebraic rewrite finishes.
why it matters
This is the integrality step for the local winding package on exact $S^1$. Immediately downstream, the normalized winding number of a loop is shown to be an integer by dividing the displacement by $2\pi$. That result is reused for singular $1$-simplices: a $1$-simplex with equal vertices has integer simplex winding, via reduction to the path statement.
In the Recognition foundation layer this supplies a clean, axiom-free integer invariant for closed paths before any homotopy or homology machinery is layered on. It does not itself invoke the forcing chain (T0–T8) or the Recognition Composition Law; it is pure covering geometry that later geometric and physical constructions can quote without reopening the deck-group argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.