edge02
plain-language theorem explainer
The geometric edge from vertex 0 to vertex 2 of the standard 2-simplex Δ², packaged as a Path. Realized by the face map δ₁ composed with the unit-interval parameterization. Downstream proofs of the winding-kills-boundaries identity cite it as the direct edge against which the broken boundary walk is compared. Construction is a Path structure whose continuous map is simplexEdge 1, with endpoints checked by the zero/one lemmas.
Claim. The edge $v_0 \to v_2$ of the standard $2$-simplex $\Delta^2$, realized as a continuous path $I \to \Delta^2$ via the face map $\delta_1$ (composed with the standard parameterization of $\Delta^1$ by the unit interval).
background
The module lifts path-level winding and displacement on $S^1$ to singular simplices, then proves that displacement vanishes on boundaries of singular $2$-simplices. That identity is the chain-level fact making winding a homology invariant and giving the split-injective half of $H_1(S^1;\mathbb{Z}) \cong \mathbb{Z}$.
Vertices of $\Delta^2$ are written $V(k) = \mathrm{stdSimplex.vertex},k$. The geometric edge selected by the $i$-th face map is $\mathrm{simplexEdge},i = (\mathrm{faceMap},i) \circ \mathrm{intervalToSimplex}$, a continuous map $I \to \Delta^2$. The lemmas $\mathrm{simplexEdge_zero}$ and $\mathrm{simplexEdge_one}$ identify the endpoints with the corresponding vertices of $\Delta^2$.
Face maps on a singular $2$-simplex $F$ produce the three singular $1$-simplices whose displacements enter the alternating sum. The edge $v_0 \to v_2$ is the direct side of the $2$-simplex telescoping argument in the module doc.
proof idea
Definitional Path structure, not a deep proof. The continuous map is set to $\mathrm{simplexEdge},1$. Source equality $\mathrm{simplexEdge},1,0 = V,0$ is rewritten by $\mathrm{simplexEdge_zero}$ then congruence on the vertex index; target equality $\mathrm{simplexEdge},1,1 = V,2$ is rewritten by $\mathrm{simplexEdge_one}$ the same way. No homotopy or displacement lemmas are invoked here.
why it matters
Supplies the direct edge $v_0 \to v_2$ used in $\mathrm{simplexDisplacement_boundary}$, the module's main theorem: for every singular $2$-simplex $F$, $\mathrm{disp}(\delta_0 F) - \mathrm{disp}(\delta_1 F) + \mathrm{disp}(\delta_2 F) = 0$. The module doc frames that identity as $2$-simplex telescoping: the broken walk $v_0 \to v_1 \to v_2$ is homotopic rel endpoints inside the convex (hence simply connected) standard $2$-simplex to this direct edge; pushing the homotopy through $F$ and using path-displacement additivity and homotopy invariance yields the vanishing alternating sum.
Together with the fact that winding sends the once-around generator to $1$, this is the "kills boundaries" half of the winding homomorphism on $1$-cycles, the split-injective side of $H_1(S^1;\mathbb{Z}) \cong \mathbb{Z}$. Generation (surjectivity of the integer comparison) still needs a simplicial prism or subdivision operator not yet in Mathlib singular homology. No Recognition forcing-chain landmarks (T5–T8, RCL, $\varphi$) are touched; this is pure foundational topology supporting the circle invariant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.