intervalReverse
plain-language theorem explainer
The continuous self-map of the unit interval sending t to 1-t. Path-reversal constructions on S¹ cite it as the reparameterization factor. It is the Mathlib unit-interval symmetry packaged as a continuous map C(I,I).
Claim. The map $t \mapsto 1-t$ on the unit interval $I=[0,1]$ is continuous, and is recorded as an element of $C(I,I)$.
background
The module builds a local winding (displacement) invariant for paths in the exact TopCat.sphere 1 object. A path $\gamma:I\to S^1$ is lifted through the covering $\mathbb{R}\to S^1$ given by the trigonometric circle map; displacement is the net travel of that lift in $\mathbb{R}$.
Reversing a path means composing with the interval flip $t\mapsto 1-t$. Mathlib already supplies unitInterval.symm and its continuity proof; this definition packages that pair as a single continuous map so later path constructions can compose against it.
No project-local circle substitute is used: everything sits on the standard covering and Mathlib's continuous-map API.
proof idea
One-line definition: the continuous-map constructor applied to Mathlib's unitInterval.symm together with the existing continuity lemma unitInterval.continuous_symm. No further proof obligations.
why it matters
Feeds reversePath, which is simply path composition with this flip, and thereby pathDisplacement_reverse: traversing a path backwards negates its displacement, because the canonical lift composed with $t\mapsto 1-t$ lifts the reversed path and the endpoint difference changes sign.
That sign-flip is the elementary orientation property of the winding invariant on $S^1$. In the broader Recognition foundation it keeps the displacement a genuine oriented invariant under path reparameterization, consistent with the covering-space deck group $2\pi\mathbb{Z}$ used throughout the module. It is pure topological scaffolding, not a forcing-chain step, but without it the reverse-path identities cannot even be stated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.