pathBacktrackMap_face_zero
plain-language theorem explainer
The 0-face of the triangular backtrack 2-simplex over a continuous path γ on S¹ is the singular 1-simplex of the reverse path t ↦ γ(1−t). Anyone assembling the free singular boundary of that prism cites this face identity. The argument is pointwise: face-0 coordinates restrict to interval reversal, so composing with γ recovers the reverse path as a 1-simplex.
Claim. For every continuous path $\gamma : I \to S^1$, the $0$-th face of the triangular backtrack singular $2$-simplex associated to $\gamma$ equals the singular $1$-simplex obtained by reading the reverse path $t \mapsto \gamma(1-t)$ through the standard homeomorphism $\Delta^1 \simeq I$.
background
This module lifts the path-level winding/displacement invariant on $S^1$ to singular simplices and proves that displacement kills boundaries: for every singular $2$-simplex $F$, the alternating face sum of displacements vanishes. That identity, with the generator evaluation on the once-around loop, supplies the split-injective half of $H_1(S^1;\mathbb{Z}) \cong \mathbb{Z}$.
The triangular backtrack prism over a path $\gamma$ is the singular $2$-simplex sending $x \in \Delta^2$ to $\gamma$ of a one-parameter coordinate on $x$. By design its three faces are the reverse path, the constant initial edge, and the original path. Faces of a $2$-simplex are obtained by composing with the standard face maps $\Delta^1 \to \Delta^2$; paths become $1$-simplices via the homeomorphism $\Delta^1 \simeq I$.
The reverse path is $\gamma$ reparameterized by $t \mapsto 1-t$. An upstream coordinate lemma records that the one-parameter coordinate, restricted along face $0$, is exactly that interval reversal composed with the standard simplex-to-interval map.
proof idea
Pointwise extensionality on the underlying maps of singular $1$-simplices. After ext x, the claim reduces to equality of two maps $\Delta^1 \to S^1$ at $x$. Both sides are $\gamma$ composed with a real coordinate on the face; the upstream identity twoSimplexCoordOneParam_face_zero says that coordinate on face $0$ is unit-interval reversal of the standard homeomorphism value. Applying congruence in $\gamma$ finishes the proof in one line.
why it matters
This is one of the three face identities that unpack the free singular boundary of the backtrack prism. The immediate parent is singularTwoBoundaryFree_freeMk_pathBacktrack, whose doc-comment states the boundary is "reverse path minus the constant initial edge plus the original path." That algebraic boundary is the chain-level witness that a path and its reverse cancel up to a null-homologous constant edge, feeding the telescoping argument behind simplexDisplacement_boundary.
In the broader Recognition foundation stack this sits inside the singular-homology computation of the circle winding invariant: the module aims at a left inverse to the fundamental class on $H_1(S^1)$, the split-injective half of $H_1(S^1;\mathbb{Z}) \cong \mathbb{Z}$. No forcing-chain landmark (T5–T8) is invoked here; the result is pure singular topology scaffolding for that comparison map. The generation/surjectivity half remains open pending a simplicial prism or subdivision operator Mathlib does not yet supply.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.