pathDisplacement_homotopic
plain-language theorem explainer
Paths on the circle that are homotopic relative to endpoints have identical displacement (the real travel of a covering lift). Anyone assembling the winding number as a homology invariant cites this: it is the mechanism that forces boundary loops to contribute zero. The proof rewrites both displacements via lift-independence, then invokes covering path-lift uniqueness for homotopies rel endpoints so the lifted endpoints coincide.
Claim. Let $\gamma,\delta:I\to S^1$ be continuous paths. If $\gamma$ and $\delta$ are homotopic relative to the endpoint set $\{0,1\}$, then their displacements agree: $\mathrm{disp}(\gamma)=\mathrm{disp}(\delta)$, where displacement is the net real travel of a lift through the trigonometric covering $\mathbb{R}\to S^1$.
background
This module equips the exact TopCat.sphere 1 carrier with a local winding invariant. Displacement of a path $\gamma$ is defined by choosing a real start angle in the fiber of the initial point, lifting $\gamma$ through the trigonometric covering map $\mathrm{trigCirclePoint}:\mathbb{R}\to S^1$, and taking the difference of the lift at the two ends of $I$.
The covering is packaged as an IsCoveringMap, so Mathlib's path-lifting API applies directly. The key upstream fact is lift independence: displacement computed from the canonical lift equals the endpoint difference of any continuous real lift of $\gamma$. Two lifts that start in the same fiber differ by a constant deck transformation in $2\pi\mathbb{Z}$, so endpoint differences coincide.
Homotopy relative to endpoints forces the paths to share their initial (and terminal) points; that shared start is used to feed both lifts the same real basepoint.
proof idea
From the relative homotopy, the two paths agree at time $0$. Rewrite both initial points as $\mathrm{trigCirclePoint}$ of the same chosen real start angle for $\gamma$. Apply the covering's liftPath_apply_one_eq_of_homotopicRel to conclude that the two lifted paths, started at that common real angle, agree at time $1$.
Express each displacement via lift independence as (lift at $1$) minus (lift at $0$). The lift-at-$0$ values both equal the shared start angle, and the lift-at-$1$ values coincide by the previous step, so the two displacements are equal.
why it matters
This is the core homotopy-invariance step for the local winding invariant on $S^1$. Downstream, simplexDisplacement_boundary uses it to prove that the alternating face sum of displacements on any singular $2$-simplex vanishes: the broken boundary walk is homotopic rel endpoints, inside the simply connected standard simplex, to the direct edge, so the telescoping sum is zero.
That vanishing is exactly what makes displacement a homology invariant (it kills boundaries). In the Recognition foundation stack this supplies the topological content behind discrete octave/period counting on the circle, feeding later forcing-chain geometry without introducing project-local $S^1$ replacements or axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.