pathDisplacement_coneTerminalSide
plain-language theorem explainer
The terminal-return edge of the cone over a continuous circle path has path displacement equal to the negative of the base path displacement. Anyone evaluating simplex winding on cone faces of singular 1-simplices cites this identity. The argument is a short algebraic reduction: feed an explicit real lift into lift-independence of displacement, then simplify and cancel.
Claim. For every continuous path $\gamma : I \to S^1$, the path displacement of the path associated to the terminal-return side of the cone over $\gamma$ equals $-$ the path displacement of $\gamma$.
background
This module lifts the path-level displacement invariant on $S^1$ to singular 1-simplices and proves that alternating face sums of displacements vanish on every singular 2-simplex (the chain-level "winding kills boundaries" identity). Displacement of a path $\gamma$ is the net travel of its canonical real lift: $\mathrm{pathLift},\gamma(1)-\mathrm{pathLift},\gamma(0)$. By lift independence, the same difference is recovered from any continuous real lift of $\gamma$.
The cone construction supplies three singular 1-simplices over a base path. The terminal-return side is the edge that runs from the cone tip back along the terminal fiber value of the base lift to the initial fiber value. Concretely it is the map sending barycentric coordinates to the trigonometric image of the affine combination $(1-x_1)\cdot\mathrm{pathLift},\gamma(1)+x_1\cdot\mathrm{pathLift},\gamma(0)$. Reparameterizing the standard 1-simplex to the unit interval turns that edge into an ordinary path on $S^1$, to which path displacement applies.
proof idea
Apply lift independence of path displacement to the reparameterized terminal-return edge, using the explicit continuous real lift $t\mapsto(1-t)\cdot\mathrm{pathLift},\gamma(1)+t\cdot\mathrm{pathLift},\gamma(0)$ and the lemma that this lift covers the edge. Unfold the lift and the definition of path displacement; the endpoint difference is $\mathrm{pathLift},\gamma(0)-\mathrm{pathLift},\gamma(1)$, which is the negative of the base displacement. Finish by ring.
why it matters
This is the displacement half of the terminal-return cone identity. The immediate parent is the winding form: simplex winding of the terminal-return side equals the negative of base path displacement divided by $2\pi$. Together with the matching identities on the other two cone edges, it feeds the 2-simplex telescoping that proves alternating face sums of displacements vanish, i.e. that simplex displacement is a homology invariant on $S^1$.
In the module's larger program that invariant, paired with the fact that the once-around generator has winding 1, supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The generation (surjectivity) half still needs a simplicial prism or subdivision operator not yet in Mathlib. The result is pure classical covering-space algebra; it does not itself invoke the RS forcing chain, but it is foundation infrastructure for any later recognition of circular phases or eight-tick windings.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.