pathDisplacement_reverse
plain-language theorem explainer
Reversing a continuous path on the circle negates its real-line displacement. Anyone computing oriented windings or checking sign-consistency of the local winding number will cite this. The argument lifts the reversed path by composing the canonical lift with interval reversal, invokes lift-independence of displacement, and flips the endpoints.
Claim. For every continuous path $\gamma:I\to S^1$, the displacement of the time-reversed path equals the negative of the displacement of $\gamma$: if $\mathrm{disp}(\gamma)$ is the endpoint difference of the canonical real lift of $\gamma$, then $\mathrm{disp}(\gamma^{\mathrm{rev}})=-\mathrm{disp}(\gamma)$.
background
This module equips paths in the exact TopCat.sphere 1 carrier with a real displacement invariant. The covering map is the once-around trigonometric parametrization sending $t\in\mathbb{R}$ to a point of $S^1$. A path $\gamma:I\to S^1$ is lifted to a continuous real path via a choice-based covering lift; displacement is then the endpoint difference of that lift.
The key upstream fact is lift independence: displacement from the canonical lift equals the endpoint difference of any continuous lift of the same path. Two lifts that start in the same fiber differ by a constant deck transformation in $2\pi\mathbb{Z}$, so endpoint differences agree. Interval reversal is the continuous self-map $t\mapsto 1-t$ on the unit interval; path reversal is reparametrization of $\gamma$ by that map.
proof idea
Build an explicit real lift of the reversed path: compose the canonical lift of $\gamma$ with interval reversal. Pointwise, the covering map applied to that composition recovers the reversed path, by the lifting property of the canonical lift evaluated at $1-t$.
Apply lift independence to rewrite the displacement of the reversed path as the endpoint difference of this composed lift. Evaluate at the reversed endpoints: $\mathrm{symm}(1)=0$ and $\mathrm{symm}(0)=1$, so the difference is $\mathrm{lift}\gamma(0)-\mathrm{lift}\gamma(1)$. That is exactly the negative of the original displacement (by the definition of displacement as endpoint difference of the canonical lift). Finish with ring.
why it matters
Sign-reversal under path reversal is the elementary orientation axiom for a winding invariant. Downstream, the chain module uses it when equating oriented winding of an oriented singular edge to normalized path displacement: the oriented path is built from an underlying edge path with a choice of orientation, and the equality must flip sign when the orientation flips.
In the broader Recognition foundation this sits under the circle-covering toolkit that makes local winding a usable invariant without project-local $S^1$ replacements. It does not itself force the eight-tick octave or $D=3$, but it is part of the topological substrate those later forcing steps rely on when counting oriented turns.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.