reversePath
plain-language theorem explainer
The reverse of a continuous path on the unit circle, reparameterized by t ↦ 1 − t. Anyone computing displacement under orientation flip, or building oriented singular edges and backtrack prisms, cites this. It is a one-line continuous composition with the unit-interval symmetry map.
Claim. Given a continuous path $\gamma : I \to S^1$, its reverse is the continuous path $t \mapsto \gamma(1-t)$ on the unit circle.
background
The module builds a local winding (displacement) invariant for paths in the exact TopCat.sphere 1 object. Paths are lifted through the trigonometric covering map to $\mathbb{R}$, and displacement is the endpoint difference of the lift. The key invariance result is that any continuous lift yields the same displacement, via deck transformations by $2\pi\mathbb{Z}$.
SphereOne is the carrier type of that exact sphere object. The unit interval $I$ is the standard path domain. The sibling map intervalReverse is the continuous self-map $t \mapsto 1-t$ on $I$ (Mathlib's unitInterval.symm). Path reverse is ordinary precomposition with that symmetry, so the reversed path runs the original trajectory backwards at unit speed.
proof idea
Pure definition: continuous composition of the given path $\gamma : C(I,S^1)$ with the continuous interval reversal $t \mapsto 1-t$. No lemmas, no tactics; the body is a single comp.
why it matters
Orientation reversal is the algebraic sign flip for the winding invariant. Downstream, pathDisplacement_reverse proves that displacement of the reversed path equals the negation of the original displacement, by lifting through the reversed canonical lift. The simp lemma reversePath_apply unpacks pointwise evaluation.
In the chain layer, oriented singular edges use this for the backward case (orientedEdgePath), and the triangular backtrack prism uses it as the reverse-path face (pathBacktrackMap_face_zero, singularTwoBoundaryFree_freeMk_pathBacktrack). Those identities feed free singular homology computations on $S^1$, where reverse-minus-constant-plus-forward is the boundary of a 2-simplex. Within Recognition Science this is foundation infrastructure for the circle covering and eight-tick/period structure, not a physics forcing step itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.