edge01
plain-language theorem explainer
The geometric edge from vertex v₀ to v₁ on the standard 2-simplex Δ², packaged as a Path, via the face map δ₂. Anyone assembling the broken boundary walk for the winding-kills-boundaries identity cites this. The body is the continuous map simplexEdge 2 with two short endpoint obligations discharged by the vertex lemmas.
Claim. The continuous path along the edge from vertex $v_0$ to vertex $v_1$ of the standard $2$-simplex $\Delta^2 \subset \mathbb{R}^3$, obtained by composing the face map $\delta_2$ with the standard reparameterization of the unit interval onto $\Delta^1$.
background
This module lifts the path-level winding and displacement invariant of the circle to singular simplices of $S^1$, and proves that the invariant kills boundaries. The key identity is that for every singular $2$-simplex $F : C(\Delta^2, S^1)$, the alternating face sum of displacements vanishes: $\mathrm{disp}(\delta_0 F) - \mathrm{disp}(\delta_1 F) + \mathrm{disp}(\delta_2 F) = 0$.
The vertices of $\Delta^2$ are written $V(k) = \mathrm{stdSimplex.vertex}, k$ for $k \in \mathrm{Fin}, 3$. The geometric edge selected by the $i$-th face map is the continuous map $\mathrm{simplexEdge}, i : C(I, \Delta^2)$, namely $(\mathrm{faceMap}, i) \circ \mathrm{intervalToSimplex}$. Face maps themselves are the topological realizations of $\mathrm{SimplexCategory.}\delta$.
The three edges of $\Delta^2$ are the building blocks of the broken boundary walk $v_0 \to v_1 \to v_2$ used in the telescoping argument.
proof idea
Definitional packaging: the underlying continuous map of the path is $\mathrm{simplexEdge}, 2$. The source obligation $\mathrm{simplexEdge}, 2, 0 = V, 0$ rewrites by $\mathrm{simplexEdge_zero}$ and a one-step congruence on vertices; the target obligation $\mathrm{simplexEdge}, 2, 1 = V, 1$ rewrites by $\mathrm{simplexEdge_one}$ the same way. No homotopy or displacement content is involved.
why it matters
Feeds the parent theorem $\mathrm{simplexDisplacement_boundary}$, the chain-level statement that winding kills boundaries. That theorem's proof compares the broken walk $v_0 \to v_1 \to v_2$ (built from the three edge paths) with the direct edge $v_0 \to v_2$ inside the simply connected standard $2$-simplex, then pushes the homotopy through $F$ and applies path-displacement additivity and homotopy invariance.
Together with the fact that the invariant sends the once-around generator to $1$, this supplies the split-injective half of $H_1(S^1;\mathbb{Z}) \cong \mathbb{Z}$. The generation (surjectivity) half still needs a simplicial prism or subdivision operator, which Mathlib singular homology does not yet provide. No Recognition-Science forcing-chain landmark (T0–T8) is touched directly; the result is pure foundational topology supporting later circle-winding arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.