simplexEdge_zero
plain-language theorem explainer
At parameter 0, each geometric edge of the standard 2-simplex lands on the vertex selected by the corresponding face map. Path constructors for the three boundary edges of Δ² cite this to discharge source endpoints. The proof is a four-step rewrite through the edge definition, the interval-to-simplex basepoint, and vertex preservation under face maps.
Claim. For every face index $i \in \{0,1,2\}$, the continuous edge map $e_i : I \to \Delta^2$ obtained by composing the $i$-th face inclusion $\delta_i : \Delta^1 \to \Delta^2$ with the standard homeomorphism $I \simeq \Delta^1$ satisfies $e_i(0) = v_{\delta_i(0)}$, the vertex of $\Delta^2$ hit by $\delta_i$ at the $0$-vertex of $\Delta^1$.
background
The module lifts path-level winding on $S^1$ to singular simplices 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 supplying the split-injective half of $H_1(S^1;\mathbb{Z}) \cong \mathbb{Z}$.
Here simplexEdge i is the geometric edge of the standard $2$-simplex selected by the $i$-th face map, realised as a continuous map $I \to \Delta^2$ by composing the face inclusion with the unit-interval parameterisation of $\Delta^1$. The three concrete boundary paths $v_0\to v_1$, $v_1\to v_2$, and $v_0\to v_2$ are built from these edges; each needs a verified source endpoint at $t=0$.
Upstream, intervalToSimplex 0 is the $0$-vertex of $\Delta^1$, faceMap i is definitionally the standard simplex map of $\delta_i$, and Mathlib's stdSimplex.map_vertex sends vertices to vertices.
proof idea
One-line rewrite wrapper. Unfold simplexEdge i 0 via simplexEdge_apply to faceMap i (intervalToSimplex 0). Replace intervalToSimplex 0 by the $0$-vertex of $\Delta^1$ using intervalToSimplex_zero. Unfold faceMap by faceMap_apply, then apply stdSimplex.map_vertex so the face map sends that vertex to the claimed vertex of $\Delta^2$.
why it matters
This is the source-endpoint lemma for the three geometric edges of $\Delta^2$. Downstream, edge01, edge12, and edge02 each invoke it (with a congr 1) to prove their Path.source' fields, so the boundary walk $v_0\to v_1\to v_2$ and the direct edge $v_0\to v_2$ are well-typed paths inside the convex $2$-simplex.
Those paths feed the $2$-simplex telescoping argument in the module doc: the two-edge walk is homotopic rel endpoints to the direct edge, and pushing the homotopy through a singular $2$-simplex $F$ plus path-displacement additivity and homotopy invariance yields simplexDisplacement_boundary. That is the kills-boundaries identity for the winding invariant on singular $1$-simplices, the key step toward a left inverse to the fundamental class on $H_1(S^1;\mathbb{Z})$.
No Recognition forcing-chain landmark (T5–T8, RCL, $\varphi$) is touched directly; the result is pure singular-homology scaffolding inside the foundation layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.