pathDisplacement
plain-language theorem explainer
Defines the real-valued displacement of a continuous path on the unit circle as the net travel of its canonical real lift: endpoint minus startpoint. Anyone working with the local winding invariant on S¹ cites this as the basic measurement. The body is a one-line difference of the covering lift at the unit-interval endpoints.
Claim. For a continuous path $\gamma : I \to S^1$, the path displacement is the real number $\widetilde{\gamma}(1) - \widetilde{\gamma}(0)$, where $\widetilde{\gamma}$ is the canonical continuous lift of $\gamma$ through the trigonometric covering $\mathbb{R} \to S^1$.
background
The module builds a local winding (displacement) invariant for paths in the exact TopCat.sphere 1 object. The circle is covered by the standard trigonometric map sending a real angle to a point of $S^1$. A continuous path $\gamma$ on the circle therefore admits continuous lifts to $\mathbb{R}$.
The sibling pathLift is the canonical such lift: it is obtained from the covering's path-lifting property, started at a chosen real preimage of $\gamma(0)$. SphereOne is simply the carrier type of that exact sphere object. Displacement is then the net change of this lift along the unit interval.
Because two lifts that start in the same fiber differ by a constant deck transformation in $2\pi\mathbb{Z}$, the endpoint difference is independent of the particular lift once the start fiber is fixed. That independence is proved later; the definition itself only records the canonical difference.
proof idea
Pure definition, not a proof. The body evaluates the already-constructed continuous lift pathLift γ at the two endpoints of the unit interval and subtracts. No tactics or lemmas are applied at this site; all covering and uniqueness work lives in pathLift and in the subsequent independence theorem.
why it matters
This is the raw numerical invariant that the rest of CircleWinding manipulates. Downstream, pathDisplacement_eq shows it equals the endpoint difference of any continuous lift, so later arguments may use convenient explicit lifts. Homotopy invariance (pathDisplacement_homotopic) makes it kill boundaries of singular 2-simplices. For closed paths it is an integer multiple of $2\pi$ (pathDisplacement_loop_intMul); the fundamental loop realizes exactly one full turn $2\pi$, giving surjectivity of the winding. Reversal negates it, and concatenation adds. Together these facts turn the covering geometry of $S^1$ into a usable integer-valued winding that the foundation layer can feed into higher Recognition constructions without project-local circle replacements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.