reversePath_apply
plain-language theorem explainer
Evaluating a reversed continuous path on the circle at parameter t recovers the original path at the reflected parameter 1-t. Anyone computing endpoints or displacements of oriented edges on S¹ cites this as the pointwise rule for path reversal. The proof is pure definitional equality (rfl): reversePath is composition with interval reversal.
Claim. For every continuous path $\gamma : I \to S^1$ and every $t \in I=[0,1]$, the reverse path satisfies $(\gamma^{\mathrm{rev}})(t)=\gamma(1-t)$, where reversal is reparameterization by $t\mapsto 1-t$.
background
The module builds the local winding (displacement) invariant for paths in the exact TopCat.sphere 1 object. A path is lifted through the trigonometric covering of the circle, and displacement is the real endpoint difference of any continuous lift. The central invariance fact is that the canonical lift's displacement agrees with that of every other lift, by a deck-transformation argument with period $2\pi\mathbb{Z}$.
SphereOne is the carrier of that sphere. The reverse of a continuous path $\gamma:I\to S^1$ is defined by composing $\gamma$ with the standard interval map $t\mapsto 1-t$. This lemma is the pointwise evaluation form of that definition, tagged @[simp] so later endpoint and orientation calculations reduce automatically.
proof idea
One-line term proof by rfl. By definition the reverse path is $\gamma$ composed with interval reversal, and that map acts on points of $I$ as unitInterval.symm (i.e. $t\mapsto 1-t$), so the stated equality is definitional.
why it matters
Used by the oriented-edge endpoint lemmas in CircleWindingChain (orientedEdgePath_zero, orientedEdgePath_one), which case-split on orientation and need reverse-path evaluation when an edge is traversed backwards. Those lemmas pin the initial and terminal $S^1$-points of singular edges under orientation, feeding the chain-level winding calculus.
In the Recognition foundation this sits under the circle-covering geometry that supports phase and winding invariants; the eight-tick octave (forcing step T7) is the discrete period structure that the continuous $S^1$ covering packages. Fully proved: no sorry, no open scaffold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.