pathDisplacement_trans
plain-language theorem explainer
Path displacement on the circle is additive under concatenation: the lift-endpoint difference of γ · γ' equals the sum of the two pieces. Algebraic topologists and anyone building the singular homology of S¹ from covering lifts would cite it. The proof lifts each path through the trigonometric covering, glues the lifts by the covering's lift-of-concatenation theorem, and cancels the intermediate endpoint by ring arithmetic.
Claim. Let $x,y,z\in S^1$ and let $\gamma$ be a path from $x$ to $y$, $\gamma'$ a path from $y$ to $z$. Then the displacement of the concatenated path equals the sum of the displacements: $\mathrm{disp}(\gamma\cdot\gamma')=\mathrm{disp}(\gamma)+\mathrm{disp}(\gamma')$, where displacement is the net travel in $\mathbb{R}$ of any continuous lift through the trigonometric covering $t\mapsto(\cos t,\sin t)$.
background
The module equips the exact TopCat.sphere 1 carrier (abbreviated SphereOne) with a local winding invariant. Paths are lifted through the trigonometric covering map trigCirclePoint : ℝ → S¹, which is an IsCoveringMap. Displacement of a continuous path γ is defined as the endpoint difference of its canonical lift: pathLift(γ)(1) − pathLift(γ)(0).
The key upstream fact is lift independence (pathDisplacement_eq): any continuous lift Γ of γ has the same endpoint difference as the canonical lift, because two lifts starting in the same fiber differ by a constant deck transformation in 2πℤ. Surjectivity of trigCirclePoint supplies a real starting angle for every base point, so every path admits a lift.
Local setting (module doc): no axioms, no sorry, and no project-local S¹ replacements; everything runs on Mathlib's covering and path-lifting API.
proof idea
Pick a real preimage e of the start point x via surjectivity of trigCirclePoint. Lift γ from e to obtain Lγ; its endpoint Lγ(1) lies over y. Lift γ' from that same real value to obtain Lγ'. Apply pathDisplacement_eq to each piece: disp(γ) = Lγ(1)−e and disp(γ') = Lγ'(1)−Lγ(1).
For the concatenation, lift γ·γ' from the same start e. The covering's lift-of-concatenation theorem (liftPath_trans) identifies the concatenated lift's endpoint with Lγ'(1). Another application of pathDisplacement_eq gives disp(γ·γ') = Lγ'(1)−e. The three identities and ring finish the proof.
why it matters
Additivity is half of what makes displacement a homology invariant on S¹; the other half is homotopy invariance. Downstream, simplexDisplacement_boundary in CircleWindingChain uses it to prove that the alternating face sum of displacements on any singular 2-simplex vanishes: the broken boundary walk telescopes to zero. The doc-comment states the intended payoff explicitly: "the alternating face sum of a singular 2-simplex telescopes to 0."
In the Recognition foundation layer this supplies the local winding calculus on the circle before global forcing (T0–T8) and the eight-tick octave are invoked. It is pure covering-space algebra, not yet a physics claim, but it is the exact identity needed so that later chain-level arguments can treat displacement as a 1-cocycle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.