edge12

The module lifts the path-level winding/displacement invariant of the circle to singular simplices of $S^1$, and proves that displacement vanishes on boundaries. A singular $1$-simplex is a continuous map $\Delta^1 \to S^1$; a singular $2$-simplex is a map $\Delta^2 \to S^1$. Displacement of a $1$-simplex is path displacement after reparameterizing $\Delta^1$ to the unit interval.

Here $V(k)$ is the $k$-th vertex of the standard $2$-simplex in $\mathbb{R}^3$. The geometric edge selected by the $i$-th face map is simplexEdge i: the composition of the topological face inclusion (skipping vertex $i$) with the standard map from the unit interval onto $\Delta^1$. Face maps $\delta_i$ are the usual simplicial face operators; $\delta_0$ skips $v_0$ and therefore runs along the edge $v_1 \to v_2$.

Definitional packaging, not a deep argument. The underlying continuous map is simplexEdge 0. The source obligation reduces by simplexEdge_zero to the image of the $0$-endpoint under the face map, which is $V,1$; the target obligation reduces by simplexEdge_one to $V,2$. Both steps finish with a one-line congruence on the vertex index.

This is one of the three named edges of $\Delta^2$ used in the telescoping proof of simplexDisplacement_boundary: for every singular $2$-simplex $F$, the alternating face sum of displacements vanishes. That identity is the chain-level statement that winding kills boundaries, and together with the fact that the fundamental loop has winding $1$ it supplies the split-injective half of $H_1(S^1;\mathbb{Z}) \cong \mathbb{Z}$.

The module doc frames the larger goal: a winding homomorphism on $1$-cycles that is a left inverse to the fundamental class. Surjectivity (every cycle homologous to an integer multiple of the generator) still needs a simplicial prism/subdivision operator not yet in Mathlib. The edge definitions are pure scaffolding for that telescoping homotopy inside the convex, simply connected standard $2$-simplex.