oneSimplexPath
plain-language theorem explainer
Converts a singular 1-simplex on S¹ into a continuous unit-interval path by precomposing with the standard homeomorphism Δ¹ ≃ I. Anyone citing simplexDisplacement, simplexWinding, or the zero-winding cone filler uses this bridge. The body is pure continuous composition; no analytic content.
Claim. Given a continuous map $f:\Delta^1\to S^1$ (a singular $1$-simplex on the circle), define the associated path $\gamma_f:I\to S^1$ by $\gamma_f=f\circ\iota$, where $\iota:I\to\Delta^1$ is the standard homeomorphism $t\mapsto(1-t,t)$.
background
The module lifts the path-level winding and displacement invariants of CircleWinding to singular simplices on $S^1=\mathrm{TopCat.sphere},1$, and proves that displacement kills boundaries of $2$-simplices. That identity is the chain-level fact making winding a homology invariant, and (with the generator evaluation) supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
A singular $1$-simplex is a continuous map $f:\Delta^1\to S^1$, where $\Delta^1=\mathrm{stdSimplex},\mathbb{R},(\mathrm{Fin},2)$. The reparameterisation $\iota:I\to\Delta^1$, $t\mapsto(1-t,t)$, is the continuous inverse of Mathlib's stdSimplexHomeomorphUnitInterval. Path-level tools (pathDisplacement, pathWinding, homotopy invariance) live on $C(I,S^1)$, so every simplex-level statement first routes through this conversion.
SphereOne is just the carrier of $\mathrm{TopCat.sphere},1$; no project-local circle replacement is used.
proof idea
One-line definitional wrapper: precompose the singular $1$-simplex $f:C(\Delta^1,S^1)$ with the fixed continuous map $\iota:I\to\Delta^1$. Continuity of the composite is immediate from continuity of both factors. No lemmas are applied beyond function composition in the continuous-map type.
why it matters
This is the standard dictionary between singular $1$-simplices and unit-interval paths on $S^1$. Downstream, every cone construction and face identity is stated on the path side: coneCirclePoint, coneLiftAngle, and coneCircleMapOfContinuous all take oneSimplexPath f; face-two recovery (coneCirclePoint_faceMap_two_of_oneSimplex, coneCircleMapOfContinuous_face_two) and side-face agreement under zero winding route through it.
The closed-edge bounding theorems (closedSingularOneCycle_bounds_of_closed_cone_map, _of_continuous_coneCirclePoint, _of_zero_winding_coneCirclePoint) use the path form to build an explicit continuous $2$-simplex filler when winding vanishes. Together with simplexDisplacement_boundary (the kills-boundaries identity) and pathWinding on the fundamental loop, this supports 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 singular homology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.