simplexEdge_one
plain-language theorem explainer
At the unit-interval endpoint t=1, the geometric edge of Δ² selected by the i-th face map lands on the vertex obtained by applying the simplicial face map δ_i to the second vertex of Δ¹. Used when packaging the three boundary edges of the standard 2-simplex as Path objects. Proof is a four-step rewrite through the definitions of simplexEdge, intervalToSimplex, and faceMap.
Claim. For every face index $i \in \{0,1,2\}$, the geometric edge map of the standard $2$-simplex associated to the $i$-th face satisfies $\mathrm{edge}_i(1) = v_{\delta_i(1)}$, where $v_k$ is the $k$-th vertex of $\Delta^2$ and $\delta_i : \Delta^1 \to \Delta^2$ is the simplicial face map skipping vertex $i$.
background
The module lifts the path-level winding/displacement invariant of the circle to singular simplices on $S^1$, and proves that displacement kills boundaries: for every singular $2$-simplex $F$, the alternating face sum of displacements vanishes. That identity is the chain-level fact making winding a homology invariant, and is the split-injective half of $H_1(S^1;\mathbb{Z}) \cong \mathbb{Z}$.
The geometric edge $\mathrm{simplexEdge}, i$ is the continuous map $I \to \Delta^2$ obtained by composing the unit-interval parameterisation of $\Delta^1$ with the topological face map induced by $\delta_i$. The face map itself is $\mathrm{stdSimplex.map}$ of the simplicial morphism $\delta_i$, so vertices of $\Delta^1$ are sent to vertices of $\Delta^2$.
Upstream, $\mathrm{intervalToSimplex}, 1$ is already identified with the second vertex of $\Delta^1$, and $\mathrm{faceMap_apply}$ is definitional equality with $\mathrm{stdSimplex.map}$. The companion statement at $t=0$ is the twin lemma used for path sources.
proof idea
Term-mode rewrite chain of four simp-friendly equalities. Unfold $\mathrm{simplexEdge}, i, 1$ via $\mathrm{simplexEdge_apply}$ to $\mathrm{faceMap}, i,(\mathrm{intervalToSimplex}, 1)$. Replace the inner point by $\mathrm{intervalToSimplex_one}$, getting the second vertex of $\Delta^1$. Apply $\mathrm{faceMap_apply}$ to turn the face map into $\mathrm{stdSimplex.map},(\delta_i)$, then finish with $\mathrm{stdSimplex.map_vertex}$, which sends vertices to vertices under the induced map.
why it matters
This endpoint identity is the target half of the three Path constructors $\mathrm{edge01}$, $\mathrm{edge02}$, and $\mathrm{edge12}$ (the geometric edges $v_0\to v_1$, $v_0\to v_2$, $v_1\to v_2$ of $\Delta^2$). Those paths are the raw material for the $2$-simplex telescoping argument in the module doc: the broken walk along two edges is homotopic rel endpoints, inside the convex (hence simply connected) standard $2$-simplex, to the direct edge, and pushing the homotopy through a singular $2$-simplex $F$ yields $\mathrm{disp}(\delta_1 F)=\mathrm{disp}(\delta_2 F)+\mathrm{disp}(\delta_0 F)$.
That vanishing of the alternating face sum is $\mathrm{simplexDisplacement_boundary}$, the chain-level "winding kills boundaries" identity. Together with the generator evaluation on the fundamental loop, it supplies the left-inverse half of the comparison $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The declaration is pure foundation scaffolding for that homology computation; it does not itself touch the forcing chain T0–T8 or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.