pathDisplacement_self
plain-language theorem explainer
For any continuous path on the circle, its displacement equals the endpoint difference of its canonical real lift. This is the definitional special case of lift-independent displacement, cited whenever winding or reversed-path identities are unfolded. The proof is pure reflexivity from the definition of displacement.
Claim. For every continuous path $\gamma : I \to S^1$, the displacement of $\gamma$ equals $\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 carrier. Paths are lifted through the trigonometric covering map, and displacement records how far the lift travels in $\mathbb{R}$.
The canonical lift of a path $\gamma$ is the continuous real-valued path produced by the covering's path-lifting theorem, started at a chosen real preimage of $\gamma(0)$. Displacement is then defined as the difference of that lift at the unit-interval endpoints. The module's central technical fact is that this number agrees with the endpoint difference of any continuous lift (deck transformations differ by a constant in $2\pi\mathbb{Z}$), so later arguments may pick convenient explicit lifts.
No axioms or project-local circle replacements are used; the construction sits on Mathlib covering theory.
proof idea
One-line term proof by rfl. Displacement is defined to be exactly the endpoint difference of the canonical lift, so the stated equality is definitional and needs no further lemmas.
why it matters
This identity is the definitional hinge used whenever displacement is rewritten as an endpoint difference. Downstream it feeds the reverse-path sign flip (traversing backwards negates displacement), the integrality theorem that a closed path has displacement in $2\pi\mathbb{Z}$, and the zero-winding endpoint coincidence used by the singular-cone construction in the winding chain. The multi-edge cyclic sum in CircleWindingChain likewise expands total displacement via the same endpoint form.
In the Recognition foundation layer this is pure covering geometry: it makes the local winding invariant computable without fixing a single lift choice, which is the prerequisite for closed-walk integrality and later continuum-bridge arguments. It does not itself touch the forcing chain (T0–T8) or the J-cost; it supplies the circle-winding toolkit those layers consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.