oneSimplexPath_face
plain-language theorem explainer
On a singular 2-simplex F of S¹, reading the i-th face as a unit-interval path equals composing F with the geometric edge of Δ² selected by that face. Anyone proving the face-displacement bridge or the 2-simplex telescoping for simplexDisplacement_boundary cites this. The proof is a one-line extensionality check: composition of continuous maps is associative.
Claim. For every continuous map $F:\Delta^2\to S^1$ and every face index $i\in\{0,1,2\}$, the unit-interval path associated to the $i$-th face $\delta_i F$ equals $F$ composed with the geometric edge of $\Delta^2$ cut out by the $i$-th face map: $\mathrm{path}(\delta_i F)=F\circ e_i$.
background
This module lifts the path-level winding/displacement invariant of CircleWinding to singular simplices of $S^1$, and proves that displacement kills boundaries: for every singular 2-simplex $F$, the alternating face sum $\mathrm{disp}(\delta_0 F)-\mathrm{disp}(\delta_1 F)+\mathrm{disp}(\delta_2 F)$ vanishes.
A TwoSimplex is a continuous map $F:\Delta^2\to S^1$ from the standard topological 2-simplex. Its $i$-th face is the singular 1-simplex $F\circ\mathrm{faceMap}_i$. The helper oneSimplexPath reparameterises a singular 1-simplex along the standard homeomorphism $\Delta^1\simeq I$, $t\mapsto(1-t,t)$. The geometric edge simplexEdge i is the same face map precomposed with that reparameterisation, so it is a continuous path in $\Delta^2$ along the edge opposite vertex $i$.
The identity here is the pure reparameterisation fact that makes faces and geometric edges interchangeable when measuring displacement.
proof idea
Term-mode proof by pointwise extensionality. Expanding definitions, the left-hand side is $(F\circ\mathrm{faceMap}_i)\circ\mathrm{intervalToSimplex}$ and the right-hand side is $F\circ(\mathrm{faceMap}_i\circ\mathrm{intervalToSimplex})$. These agree by associativity of continuous-map composition, so ext t; rfl closes the goal with no further lemmas.
why it matters
This is the reparameterisation bridge used immediately by simplexDisplacement_face, whose doc-comment states: the face displacement equals the displacement of the edge path pushed through $F$, "the bridge between the singular-simplex face and the geometric edge used in the telescoping."
That face identity feeds the module's main theorem simplexDisplacement_boundary: the alternating face sum of displacements on any 2-simplex is zero. The module doc frames the argument as 2-simplex telescoping inside the convex (hence simply connected) standard simplex, combining path-displacement additivity with 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}$.
In the Recognition foundation stack this is pure singular-homology bookkeeping on $S^1$, not a forcing-chain step (T0–T8); it underwrites the circle winding used later as a topological invariant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.