intervalToSimplex_coord_one
plain-language theorem explainer
The affine map sending the unit interval to the standard 1-simplex via t ↦ (1−t, t) has second barycentric coordinate exactly t. Anyone computing path displacements or cone fillers on singular 1-simplices of S¹ cites this coordinate identity. The proof is definitional reflexivity.
Claim. For every $t$ in the unit interval $I$, the second barycentric coordinate of the standard affine reparameterisation $t \mapsto (1-t,\, t)$ into $\Delta^1 = \mathrm{stdSimplex}\,\mathbb{R}\,(\mathrm{Fin}\,2)$ equals $t$ itself (as a real).
background
This module lifts the path-level winding/displacement invariant of CircleWinding to singular simplices of $S^1$, and proves that displacement vanishes on boundaries of 2-simplices (the chain-level "winding kills boundaries" identity). The bridge from paths on $I$ to singular 1-simplices is the continuous reparameterisation of the unit interval onto the standard 1-simplex $\Delta^1$.
That map, written intervalToSimplex, is the inverse of Mathlib's stdSimplexHomeomorphUnitInterval and is the affine embedding $t \mapsto (1-t,, t)$ into barycentric coordinates on $\mathrm{Fin},2$. The two coordinates sum to 1 and are nonnegative, so the image lands in the standard simplex. Downstream constructions (simplexDisplacement, cone base parameters, lifted cone angles) repeatedly need the second coordinate to recover the original interval parameter.
proof idea
One-line term proof by rfl. Unfolding intervalToSimplex yields the symmetric homeomorphism, whose second barycentric coordinate is definitionally $t$, so the equality is by reflexivity of equality on $\mathbb{R}$.
why it matters
This coordinate identity is the workhorse that lets every subsequent simplex-edge computation recover the unit-interval parameter. It is applied directly in coneBaseParam_simplexEdge_two_coe (base edge of the cone equals the interval parameter), coneLiftAngle_simplexEdge_one and coneLiftAngle_simplexEdge_zero_of_lift_endpoint_eq (side-face cone angles reduce via the second coordinate), oneSimplexPath_fundamental (the fundamental singular 1-simplex reads as the once-around loop precisely because the second coordinate is $t$), and stdSimplexHomeomorphUnitInterval_coe (the inverse homeomorphism extracts coordinate 1).
In the module's larger program, these facts feed the telescoping argument that simplexDisplacement vanishes on boundaries, giving the split-injective half of $H_1(S^1;\mathbb{Z}) \cong \mathbb{Z}$ together with pathWinding_fundamentalLoop. That homology comparison is the topological backbone for the circle's winding invariant in the Recognition foundation stack; the generation/surjectivity half remains open pending a simplicial prism operator.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.