intervalToSimplex_one
plain-language theorem explainer
The unit-interval endpoint t = 1 maps under the standard reparameterisation to the second vertex of Δ¹. Anyone tracking path endpoints of singular 1-simplices, edge face maps on Δ², or loop-integral winding cites this endpoint identity. The proof inverts Mathlib's simplex–interval homeomorphism at the known image of that vertex.
Claim. The continuous reparameterisation $I \to \Delta^1$ given by $t \mapsto (1-t,\, t)$ sends the right endpoint $t = 1$ to the standard vertex $e_1 = (0,1)$ of $\Delta^1$.
background
This module lifts the path-level winding and displacement invariants of CircleWinding to singular simplices of $S^1$, and proves that displacement kills boundaries: the alternating face sum of any singular 2-simplex vanishes. That chain-level identity, together with the once-around generator having winding 1, supplies the split-injective half of $H_1(S^1;\mathbb{Z}) \cong \mathbb{Z}$.
The bridge from paths on the unit interval $I$ to maps out of the standard 1-simplex $\Delta^1$ is the continuous reparameterisation $t \mapsto (1-t,, t)$. By definition it is the inverse of Mathlib's stdSimplexHomeomorphUnitInterval. Evaluating that map at the two endpoints of $I$ pins the two vertices of $\Delta^1$, which every subsequent edge-path and face-map computation needs.
The companion identity at $t = 0$ is already available; the present statement is the matching right-endpoint fact.
proof idea
Short algebraic inversion. Mathlib already knows that the forward homeomorphism sends the second standard vertex of $\Delta^1$ to $1 \in I$. Unfold the definition of the reparameterisation (it is exactly the inverse homeomorphism), rewrite the goal as an application of that inverse, and cancel by Homeomorph.symm_apply_apply.
why it matters
Endpoint bookkeeping for the singular-simplex winding chain. Downstream, simplexEdge_one uses it to identify the image of $t = 1$ under each edge of $\Delta^2$ with the corresponding face-map vertex; singularEdgePath_one uses it to match the terminal point of a singular edge path with the $S^1$-point of its terminal 0-face; and simplexWinding_loop_integral rewrites both endpoints of a closed singular 1-simplex so that path-level integer winding applies.
Those lemmas feed the module's main story: displacement is a homology invariant on singular 1-chains, and with the fundamental loop of winding 1 it realises the left-inverse half of $H_1(S^1;\mathbb{Z}) \cong \mathbb{Z}$. The generation (surjectivity) half still needs a simplicial prism or subdivision operator that Mathlib does not yet supply. No Recognition-Science forcing step (T5–T8) is touched here; the result is pure topological scaffolding for the circle's first homology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.