V
plain-language theorem explainer
Names the three corners of the standard geometric 2-simplex Δ² by index k ∈ {0,1,2}. Anyone reading the singular-simplex winding chain uses it to write the boundary walk v₀→v₁→v₂ versus the direct edge v₀→v₂. It is a one-line abbreviation of Mathlib's standard-simplex vertex constructor.
Claim. For each $k \in \{0,1,2\}$, $V(k)$ denotes the $k$-th vertex of the standard $2$-simplex $\Delta^2 = \mathrm{stdSimplex}\,\mathbb{R}\,(\mathrm{Fin}\,3) \subset \mathbb{R}^{\{0,1,2\}}$.
background
The ambient module lifts path-level winding on $S^1$ to singular simplices and proves that displacement kills boundaries. A singular $1$-simplex is a continuous map $f:\Delta^1\to S^1$; a singular $2$-simplex is $F:\Delta^2\to S^1$. Displacement of a $1$-simplex is path displacement after reparameterizing $\Delta^1$ to the unit interval.
The standard $2$-simplex $\Delta^2$ is the convex set of nonnegative triples summing to $1$. Its three vertices are the standard basis points. The module's telescoping argument compares the two-edge boundary walk along those vertices with the direct edge, using convexity (hence simple connectedness) of $\Delta^2$.
This abbreviation is local notation for Mathlib's stdSimplex.vertex, not the unrelated Fin 12 label used in the Freudenthal two-cube strip geometry.
proof idea
Pure definitional abbreviation: expand to Mathlib's vertex map sending $k:\mathrm{Fin},3$ to the corresponding extreme point of $\Delta^2$. No proof obligations.
why it matters
The kills-boundaries identity (simplexDisplacement_boundary) is the chain-level fact that makes winding a homology invariant: for every singular $2$-simplex $F$, $\mathrm{disp}(\partial_0 F)-\mathrm{disp}(\partial_1 F)+\mathrm{disp}(\partial_2 F)=0$. The proof is $2$-simplex telescoping: the walk $v_0\to v_1\to v_2$ is homotopic rel endpoints inside $\Delta^2$ to $v_0\to v_2$; push the homotopy through $F$ and apply path-displacement additivity and homotopy invariance.
Naming those corners cleanly is bookkeeping for that telescoping and for the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ (winding sends the fundamental loop to $1$). Surjectivity still needs a prism/subdivision operator Mathlib singular homology does not yet supply. Framework-wise this sits in the topological foundation under the circle, not in the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.