SphereOne

The CircleWinding module builds a local winding (displacement) invariant for paths in the exact Mathlib 1-sphere. Paths are continuous maps $I \to S^1$; their lifts through the trigonometric covering live in $\mathbb{R}$, and displacement is the endpoint difference of a lift.

SphereOne is only a readability alias for that carrier type. The covering map itself is the once-around trigonometric parametrization: every real angle $t$ is sent to a point of $\mathrm{TopCat.sphere},1$ via the standard $(\cos t, \sin t)$ embedding (up to the usual ULift packaging). No custom $S^1$ replacement is introduced anywhere in the module.

The module's central claim is lift-independence of displacement: 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 endpoint differences agree.

Pure abbreviation: the right-hand side is Mathlib's TopCat.sphere 1. No tactics, no lemmas, no obligations.

This alias is the ambient space for the whole local winding package. Downstream definitions and theorems that mention it include the fundamental once-around loop, the canonical path lift and its displacement, lift-independence of displacement, homotopy invariance of displacement (the mechanism that kills boundaries of singular 2-simplices), and the integrality statement that a closed path has displacement in $2\pi\mathbb{Z}$.

In the Recognition foundation layer this supplies a Mathlib-native $S^1$ on which covering-space arguments run without axioms or sorry. The winding invariant is the discrete bookkeeping ingredient behind period and octave structure later in the forcing chain; the present declaration simply fixes the geometric stage those arguments act on.