pathDisplacement_eq
plain-language theorem explainer
Any continuous lift Γ of a path γ on S¹ has the same endpoint difference Γ(1)−Γ(0) as the displacement computed from the canonical lift. This is the lift-independence lemma that makes the local winding number a well-defined path invariant. The proof is the standard deck-group argument: two lifts differ by a constant in 2πℤ, so endpoint differences agree.
Claim. Let $\gamma:I\to S^1$ be continuous and let $\Gamma:I\to\mathbb{R}$ be any continuous lift, i.e. $\mathrm{trig}\circ\Gamma=\gamma$. Then the path displacement of $\gamma$ equals the endpoint difference of $\Gamma$: $\mathrm{disp}(\gamma)=\Gamma(1)-\Gamma(0)$.
background
This module builds the local winding (displacement) invariant for paths in the exact TopCat.sphere 1 object. The covering map is the standard trigonometric projection $\mathrm{trig}:\mathbb{R}\to S^1$, packaged as an IsCoveringMap via isCoveringMap_trig. A continuous lift of a path $\gamma$ is any continuous $\Gamma:I\to\mathbb{R}$ with $\mathrm{trig}\circ\Gamma=\gamma$.
The displacement of $\gamma$ is defined from a canonical (choice-based) lift pathLift γ as the real endpoint difference of that lift. For the invariant to be usable, that number must not depend on the choice of lift: every later computation should be free to pick whatever explicit lift is convenient.
The deck group of the covering is $2\pi\mathbb{Z}$. Period invariance (trigCirclePoint_add_intMul_period) and the fiber criterion (trigCirclePoint_eq_iff) identify when two real angles project to the same point of $S^1$. Lift uniqueness on the connected interval $I$ is supplied by IsCoveringMap.eq_of_comp_eq.
proof idea
Write $\Gamma'$ for the canonical lift pathLift γ. Both $\Gamma(0)$ and $\Gamma'(0)$ lie over $\gamma(0)$, so trigCirclePoint_eq_iff yields an integer $k$ with $\Gamma(0)=\Gamma'(0)+k\cdot 2\pi$. Set $c:=k\cdot 2\pi$.
The shifted map $t\mapsto\Gamma'(t)+c$ still lifts $\gamma$ by period invariance of trigCirclePoint, and it agrees with $\Gamma$ at $t=0$. Covering uniqueness (isCoveringMap_trig.eq_of_comp_eq) on the connected interval forces $\Gamma(t)=\Gamma'(t)+c$ for all $t$. Evaluating at the endpoints and cancelling $c$ gives $\Gamma(1)-\Gamma(0)=\Gamma'(1)-\Gamma'(0)$, which is the definition of path displacement.
why it matters
This is the central technical result of the CircleWinding module: without lift independence the displacement would be an artifact of the canonical choice rather than a path invariant. Downstream, it is the rewrite used to evaluate concrete lifts.
It feeds pathDisplacement_fundamentalLoop (displacement of the generator is exactly one full turn $2\pi$, the surjectivity witness), pathDisplacement_reverse (reversal negates displacement), pathDisplacement_trans (additivity under concatenation), and pathDisplacement_homotopic (homotopy invariance relative to endpoints). Together those make winding a homology invariant: the alternating face sum of a singular 2-simplex telescopes to zero. The cone-chain lemma pathDisplacement_coneTerminalSide likewise rewrites through this equality.
In the broader foundation layer this supplies the local integer-valued winding needed before global topological or Recognition-chain arguments that rely on $S^1$ covering data. No axioms or sorry appear.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.