pathBacktrackMap_face_two
plain-language theorem explainer
The second face of the triangular backtrack prism over a continuous path γ on S¹ is exactly the singular 1-simplex of γ. Anyone computing the singular boundary of that prism cites this face identity. The proof is a one-line pointwise congruence through the coordinate identity on face map 2.
Claim. For every continuous path $\gamma : I \to S^1$, the face $\delta_2$ of the triangular backtrack $2$-simplex associated to $\gamma$ equals the singular $1$-simplex obtained by reading $\gamma$ through the standard homeomorphism $\Delta^1 \simeq I$.
background
The module lifts path-level winding on $S^1$ to singular simplices and proves that displacement kills boundaries: for every singular $2$-simplex $F$, $\mathrm{disp}(\delta_0 F)-\mathrm{disp}(\delta_1 F)+\mathrm{disp}(\delta_2 F)=0$. That identity, with the generator evaluation, supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
pathBacktrackMap γ is the triangular backtrack prism: it sends $x\in\Delta^2$ to $\gamma(x_1)$. Its three faces are the reversed path, the constant initial edge, and the original path. Faces of a singular $2$-simplex are compositions with the topological face maps $\Delta^1\to\Delta^2$. oneSimplexOfPath converts a unit-interval path into a singular $1$-simplex via $\Delta^1\simeq I$.
The coordinate lemma twoSimplexCoordOneParam_face_two states that the one-parameter coordinate on $\Delta^2$, restricted along face map $2$, recovers the standard homeomorphism $\Delta^1\to I$.
proof idea
Pointwise extensionality on the singular $1$-simplex. After ext x, both sides are maps $\Delta^1\to S^1$; the left side is $\gamma$ of the one-parameter coordinate of face map $2$ applied to $x$, and the right side is $\gamma$ of the standard homeomorphism applied to $x$. The coordinate identity twoSimplexCoordOneParam_face_two equates those real parameters, so congrArg γ finishes.
why it matters
Feeds singularTwoBoundaryFree_freeMk_pathBacktrack, which records the free singular boundary of the backtrack prism as reverse path minus constant initial edge plus original path. That boundary formula is the chain-level witness that a path and its reverse cancel against a constant edge in singular $1$-chains, the elementary relation used when showing winding (displacement) vanishes on boundaries and hence descends to homology.
In the module narrative this is scaffolding for the kills-boundaries identity and the split injection $H_1(S^1;\mathbb{Z})\hookrightarrow\mathbb{Z}$. It does not itself touch the Recognition forcing chain (T5–T8) or the mass ladder; it is pure foundational topology supporting the circle winding invariant that later interfaces with RS discrete structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.