pathLift_endpoint_eq_of_winding_zero
plain-language theorem explainer
Zero winding number of a continuous path on S¹ forces the canonical real lift to close: its values at the interval endpoints coincide. Homotopy and singular-cone arguments cite this as the lift-level form of null-homotopy. The proof reduces winding to displacement via division by 2π, then reads off the endpoint difference of the canonical lift.
Claim. Let $\gamma:I\to S^1$ be continuous. If the path winding number of $\gamma$ vanishes, then the canonical lift $\widetilde{\gamma}:I\to\mathbb{R}$ satisfies $\widetilde{\gamma}(1)=\widetilde{\gamma}(0)$.
background
The module equips paths in the exact TopCat.sphere 1 carrier with a winding/displacement invariant by lifting through the trigonometric covering $\mathbb{R}\to S^1$ and measuring travel in $\mathbb{R}$. The covering is the standard angle map; deck transformations are translations by $2\pi\mathbb{Z}$.
Displacement of a path $\gamma$ is the endpoint difference of its canonical lift: $\mathrm{disp}(\gamma)=\widetilde{\gamma}(1)-\widetilde{\gamma}(0)$. Winding is that displacement divided by $2\pi$. The key upstream fact is lift independence: displacement from the canonical lift equals the endpoint difference of any continuous lift, because two lifts starting in the same fiber differ by a constant deck element (covering uniqueness plus period invariance of the trig map).
This lemma is the special case needed when winding is zero: the lift must start and end at the same real value, so it is available for linear contraction in the cover before projecting back.
proof idea
From $\mathrm{wind}(\gamma)=0$, unfold the definition of winding as $\mathrm{disp}(\gamma)/(2\pi)$. Since $2\pi\neq 0$, the division-by-zero dichotomy forces $\mathrm{disp}(\gamma)=0$. Rewrite via the reflexivity lemma that displacement of the canonical lift is exactly $\widetilde{\gamma}(1)-\widetilde{\gamma}(0)$, then close by linear arithmetic.
why it matters
This is the lift-level form consumed by the singular cone construction in CircleWindingChain. Downstream, it feeds the relative null-homotopy of closed zero-winding loops: the homotopy lifts $\gamma$ to $\mathbb{R}$, uses endpoint agreement, contracts the lift linearly to its initial value, and projects back through the covering.
It also discharges the zero-winding side-face and terminal-return identities for the cone over a singular edge: equal lift endpoints make opposite cone faces agree pointwise and collapse the terminal side to the constant apex edge. In the broader foundation layer this is pure covering-space bookkeeping (no RS constants or forcing-chain steps), but it is the analytic hinge that lets singular cones treat null-winding 1-simplices as contractible data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.