simplexToI_face_v0
plain-language theorem explainer
The unit-interval image of the two faces of the standard 0-simplex vertex is the endpoint pair {0,1}: face 0 maps to 1 and face 1 maps to 0. Anyone computing boundaries of path simplices in singular chains cites this. The proof is a short case split on the face index after reducing via the coordinate identity for the prism face of v0.
Claim. For each face index $k\in\{0,1\}$, the homeomorphism $\Delta^1\simeq I$ sends the $k$-th topological face of the unique $0$-simplex vertex $v_0$ to the endpoint $1$ if $k=0$ and to $0$ otherwise: $\mathrm{simplexToI}(\mathrm{face}_k(v_0))=\mathbf{1}_{k=0}$.
background
The module builds singular-chain infrastructure for spheres and path spaces: standard simplices $\Delta^n\subset\mathbb{R}^{n+1}$, prism face inclusions, and the identification of $\Delta^1$ with the unit interval $I$.
Here $v_0$ is the unique point of $\Delta^0$ (the Dirac mass at the single vertex). The prism face map $\mathrm{face}_k:\Delta^0\to\Delta^1$ is the topological realization of the simplicial face operator that skips vertex $k$. The continuous map $\mathrm{simplexToI}:\Delta^1\to I$ is the standard homeomorphism sending barycentric coordinates to the interval parameter.
The upstream coordinate lemma already records the raw barycentric value: the second coordinate of $\mathrm{face}_k(v_0)$ equals $1$ when $k=0$ and $0$ otherwise. The present statement simply transports that identity across the homeomorphism to $I$.
proof idea
Apply subtype extensionality so the goal becomes an equality of real numbers in $I$. Unfolding the homeomorphism reduces the claim to the second barycentric coordinate of the face, which is exactly the statement of coord_face_v0. Case-split on whether the face index equals zero; both branches rewrite the two matching if expressions and finish by reflexivity.
why it matters
Path simplices are the singular 1-chains that realize continuous paths. Their faces must land on the path endpoints so that the singular boundary recovers $\partial[\gamma]=[y]-[x]$. Downstream, pointOf_δ_pathSimplex quotes this lemma to obtain precisely that endpoint evaluation, and the module doc then packages the result as the boundary formula for a path simplex.
In the broader Recognition foundation stack this is pure singular-homology scaffolding (imports Mayer–Vietoris, prism, subdivision). It does not itself invoke the forcing chain T0–T8, the J-cost, or the eight-tick octave; it supplies the elementary geometric identity those later topological arguments need when they reduce sphere or circle windings to path boundaries.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.