simplexDisplacement_face
plain-language theorem explainer
On a singular 2-simplex F of S¹, the displacement of the i-th face equals the path displacement of any unit-interval edge path that realises the geometric face edge, after pushing that path through F. Anyone proving that winding kills 2-boundaries cites this bridge. The proof rewrites the simplex displacement definition, applies the face-path identification, and matches pointwise via the edge hypothesis.
Claim. Let $F:\Delta^2\to S^1$ be continuous and let $i\in\{0,1,2\}$. If $e:I\to\Delta^2$ is a path from $a$ to $b$ whose underlying continuous map equals the geometric $i$-th edge of $\Delta^2$, then the displacement of the singular 1-simplex $\delta_i F$ equals the path displacement of $F\circ e:I\to S^1$.
background
This module lifts the path-level winding/displacement invariant on $S^1$ to singular simplices and proves that the resulting assignment kills boundaries. A singular 2-simplex is a continuous map $F:\Delta^2\to S^1$ with $\Delta^2=\mathrm{stdSimplex},\mathbb{R}(\mathrm{Fin},3)$. Its $i$-th face is the singular 1-simplex obtained by composing $F$ with the standard face map.
Displacement of a path $\gamma:I\to S^1$ is the endpoint difference of its canonical real lift: $\mathrm{pathLift},\gamma(1)-\mathrm{pathLift},\gamma(0)$. Displacement of a singular 1-simplex is that quantity after reparameterising $\Delta^1$ onto the unit interval. The geometric edge selected by face $i$ is the continuous map $\mathrm{simplexEdge},i:I\to\Delta^2$.
Upstream, the face-path identity states that reading $\delta_i F$ in unit-interval coordinates is exactly $F$ composed with that geometric edge. The present lemma upgrades that identification from paths to displacements.
proof idea
Unfold simplex displacement to path displacement of the unit-interval reparameterisation of the face. Rewrite that reparameterisation via the face-path identity, so the left side becomes path displacement of $F\circ\mathrm{simplexEdge},i$. Congruence on the path argument, then pointwise equality on $I$: the hypothesis that $e$ realises the geometric edge gives $F(\mathrm{simplexEdge},i,t)=F(e,t)$. No homotopy or covering theory is used here; it is pure definitional transport.
why it matters
The parent theorem is the kills-boundaries identity: for every singular 2-simplex $F$, the alternating face sum of displacements vanishes. That identity is the chain-level fact making displacement a homology invariant on 1-cycles of $S^1$. The present lemma is the bridge that converts each face displacement into the displacement of a concrete geometric edge path pushed through $F$, which the telescoping argument then compares by homotopy inside the simply connected standard 2-simplex.
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 module notes that the converse generation half still needs a simplicial prism/subdivision operator not yet in Mathlib. In the Recognition foundation stack this is pure topological infrastructure for the circle covering and winding, not a direct T0–T8 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.