pathBacktrackMap_face_one
plain-language theorem explainer
The middle face of the triangular backtrack 2-simplex over a path γ on S¹ is the constant singular edge at γ's start point. Anyone assembling the free singular boundary of that prism cites this face identity. The proof is a pointwise congruence: the one-parameter coordinate vanishes on face 1, so γ is evaluated only at 0.
Claim. For every continuous path $\gamma : I \to S^1$, the face $\partial_1$ of the triangular backtrack 2-simplex associated to $\gamma$ equals the constant singular 1-simplex at $\gamma(0)$.
background
This module lifts path-level winding on $S^1$ to singular simplices and proves that displacement kills boundaries, the chain-level fact behind a left inverse $H_1(S^1;\mathbb{Z})\to\mathbb{Z}$.
A singular 2-simplex is a continuous map $F:\Delta^2\to S^1$. Its $i$-th face is $F\circ\mathrm{faceMap}_i$, a singular 1-simplex. The backtrack map over $\gamma$ sends $x\in\Delta^2$ to $\gamma$ of a one-parameter coordinate on $\Delta^2$; by design its three faces are the reverse path, a constant initial edge, and the original path.
The constant singular edge at a point $p\in S^1$ is the continuous map $\Delta^1\to S^1$ with value $p$ everywhere. The supporting coordinate lemma states that the one-parameter coordinate is identically zero on face 1 of $\Delta^2$.
proof idea
Term-mode, two steps. Extensionality on the standard 1-simplex reduces equality of continuous maps to pointwise equality. At each $x$, the face of the backtrack map is $\gamma$ applied to the one-parameter coordinate of $\mathrm{faceMap}_1(x)$. The lemma twoSimplexCoordOneParam_face_one says that coordinate is $0$, so the value is $\gamma(0)$, matching the constant edge. The argument is pure congruence under $\gamma$.
why it matters
Feeds singularTwoBoundaryFree_freeMk_pathBacktrack, which computes the free singular 2-boundary of the backtrack prism as reverse path minus constant initial edge plus original path. That identity is the algebraic witness that a path and its reverse cancel up to a null-homologous constant edge in the free chain complex.
In the module's program this is part of the chain-level "winding kills boundaries" package: once faces of the backtrack prism are identified, displacement additivity and homotopy invariance give the alternating face sum zero on every singular 2-simplex. Together with the fundamental loop having winding 1, one obtains the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The generation half still needs a prism/subdivision operator Mathlib does not yet supply.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.