pathWinding
plain-language theorem explainer
Winding number of a continuous path on S¹ equals the real displacement of its canonical covering lift, divided by 2π. Anyone citing the covering-space invariant on the circle, the integer-valued loop winding, or the zero-winding contraction uses this normalization. It is a one-line definitional rescaling of path displacement.
Claim. For a continuous path $\gamma : I \to S^1$, the winding number is the displacement of its canonical real lift divided by one full turn: $W(\gamma) := \bigl(\widetilde{\gamma}(1) - \widetilde{\gamma}(0)\bigr)/(2\pi)$, where $\widetilde{\gamma}$ is the chosen lift through the trigonometric covering $\mathbb{R}\to S^1$.
background
This module equips the exact TopCat.sphere 1 carrier (abbreviated SphereOne) with a local winding invariant. Paths are lifted through the covering map trigCirclePoint : ℝ → S¹, and displacement is read in the real line.
Upstream, path displacement is defined as the endpoint difference of the canonical lift: $\mathrm{disp}(\gamma) = \widetilde{\gamma}(1) - \widetilde{\gamma}(0)$. The key prior fact is lift independence: that difference agrees for any continuous lift of $\gamma$, because two lifts starting in the same fiber differ by a constant deck transformation in $2\pi\mathbb{Z}$. The module uses no axioms and no project-local substitute for $S^1$.
Winding is simply that displacement measured in units of one full turn $2\pi$. Closed paths then have integer winding; the fundamental once-around loop has winding $1$.
proof idea
Pure definition: unfold to path displacement divided by $2\pi$. No tactics, no lemmas. Downstream proofs that need the integer or zero-winding form typically unfold pathWinding, cancel the nonzero factor $2\pi$ by positivity, and reduce to the corresponding statement about path displacement.
why it matters
This is the normalized form of the covering invariant that later arguments actually quote. It feeds the integer-winding theorem for closed paths, the identity that the fundamental loop has winding $1$ (so winding is a left inverse to the generator), and the zero-winding endpoint equality for the canonical lift.
Those facts drive the homotopy: a closed path of winding zero is homotopic rel endpoints to the constant path at its basepoint, by lifting, contracting linearly in $\mathbb{R}$, and projecting. The same zero-winding package is consumed in CircleWindingChain for cone side-face equalities, collapse of the terminal cone side to a constant edge, and singular-edge contraction. That chain supplies the injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ (distinct multiples of the once-around loop are never homologous). Surjectivity of the fundamental class remains a separate open generation step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.