intervalToSimplex_zero
plain-language theorem explainer
At the left endpoint of the unit interval, the standard reparameterisation onto Δ¹ lands on the 0-vertex of the 1-simplex. Anyone tracking path endpoints through singular 1-simplices on S¹ cites this. The proof is a short homeomorphism cancellation: the Mathlib unit-interval homeomorphism sends vertex 0 to 0, so its inverse sends 0 back to that vertex.
Claim. The continuous map $I \to \Delta^1$ given by $t \mapsto (1-t,\, t)$ (inverse of Mathlib's standard homeomorphism $\Delta^1 \simeq I$) sends $0$ to the $0$-vertex of the standard $1$-simplex: $\iota(0) = v_0$.
background
This module lifts the path-level winding/displacement invariant of CircleWinding to singular simplices of $S^1$, and proves that displacement kills boundaries of singular 2-simplices. That identity is the chain-level fact making winding a homology invariant, and (with the generator evaluation) gives the split-injective half of $H_1(S^1;\mathbb{Z}) \cong \mathbb{Z}$.
The map intervalToSimplex is the continuous reparameterisation $I \to \Delta^1$, $t \mapsto (1-t, t)$, defined as the inverse of Mathlib's stdSimplexHomeomorphUnitInterval. Singular 1-simplices are continuous maps $\Delta^1 \to S^1$; composing with this reparameterisation turns them into ordinary paths on the unit interval so that path displacement and winding apply.
The companion evaluation at the right endpoint is the twin fact that $\iota(1)$ is the $1$-vertex. Together they pin the endpoints of every singular edge path.
proof idea
Term-style short calculation. First recall Mathlib's fact that the standard homeomorphism $\Delta^1 \simeq I$ sends the $0$-vertex to $0$. Unfold the definition of the reparameterisation via the simp lemma that identifies it with the homeomorphism inverse. Rewrite using that vertex evaluation and cancel by Homeomorph.symm_apply_apply, which recovers the vertex from applying the homeomorphism and then its inverse.
why it matters
Endpoint bookkeeping for the singular-simplex winding pipeline. Downstream, simplexEdge_zero uses it to identify the initial point of each face edge of a 2-simplex with the image of the corresponding 0-vertex under the face map; singularEdgePath_zero uses it to show that the path associated to a singular 1-simplex starts at the $S^1$-point of its initial 0-face; and simplexWinding_loop_integral needs both endpoint evaluations to reduce closed singular 1-simplices to ordinary loops and conclude integer winding.
In the module's larger story this is scaffolding for the kills-boundaries identity (simplexDisplacement_boundary) and the left-inverse half of $H_1(S^1;\mathbb{Z}) \cong \mathbb{Z}$. It does not itself touch the Recognition forcing chain (T0–T8) or the J-cost; it is pure singular-homology infrastructure that the circle-winding comparison rests on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.