pathHomotopicRel_const_of_loop_winding_zero
plain-language theorem explainer
A closed continuous path on the unit circle with vanishing winding number is homotopic relative to its endpoints to the constant path at the basepoint. Algebraic topologists and anyone building singular-chain null-homotopies on S¹ cite this. The proof lifts through the trigonometric covering, uses zero winding to equate lift endpoints, then contracts the lift linearly and projects back.
Claim. Let $\gamma: I \to S^1$ be continuous with $\gamma(1)=\gamma(0)$ and path winding number zero. Then $\gamma$ is homotopic relative to $\{0,1\}$ to the constant path at $\gamma(0)$.
background
This module equips the exact TopCat.sphere 1 carrier with a local winding (displacement) invariant. Paths are lifted through the trigonometric covering map $\mathbb{R}\to S^1$, $t\mapsto(\cos t,\sin t)$, and displacement is the net travel of the lift in $\mathbb{R}$.
The key upstream fact is that displacement is independent of lift choice: any two continuous lifts of one path that start in the same fiber differ by a constant deck transformation $2\pi\mathbb{Z}$. Consequently the endpoint difference of the canonical lift equals that of any convenient lift, so winding is a well-defined path invariant.
Here $S^1$ is the carrier of the exact sphere object, and the covering is continuous and surjective. Zero winding means the chosen lift closes: its values at the two endpoints of $I$ agree.
proof idea
From zero winding, the lift endpoints coincide: $\widetilde{\gamma}(1)=\widetilde{\gamma}(0)$. Build a straight-line homotopy in the cover, $$H(s,t)=\operatorname{trig}\bigl((1-s),\widetilde{\gamma}(t)+s,\widetilde{\gamma}(0)\bigr),$$ and project by the covering map. At $s=0$ this recovers $\gamma$ because the lift covers $\gamma$; at $s=1$ it is constantly $\gamma(0)$. On the fixed set ${0,1}$ the linear combination collapses (using endpoint equality of the lift and the loop condition $\gamma(1)=\gamma(0)$), so the homotopy is relative to endpoints. Continuity is composition of continuous maps.
why it matters
This is the path-level null-homotopy for zero-winding loops on $S^1$. Downstream it feeds singularEdgePath_homotopicRel_const_of_loop_winding_zero, which lifts the statement to singular 1-simplices and supplies the null-homotopy input for the singular prism construction on the circle.
In the Recognition foundation layer, controlled winding on the circle underwrites discrete period structure (the eight-tick octave and related covering arguments). The result is fully proved: no sorry, no extra axioms, and it uses only the standard covering lift uniqueness already established in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.