pathBacktrackMap
plain-language theorem explainer
Builds the continuous triangular backtrack prism that sends a path γ on S¹ to a singular 2-simplex by evaluating γ on the middle barycentric coordinate of Δ². Algebraic topologists cite it when manufacturing a 2-chain whose faces are γ, the reverse of γ, and a constant edge. Continuity is immediate: compose γ with the continuous one-parameter coordinate map on the standard 2-simplex.
Claim. Given a continuous path $\gamma : I \to S^1$, there is a continuous map $F_\gamma : \Delta^2 \to S^1$ defined by $F_\gamma(x) = \gamma(x_1)$, where $x_1$ is the middle barycentric coordinate of $x \in \Delta^2 = \mathrm{stdSimplex}\,\mathbb{R}(\mathrm{Fin}\,3)$.
background
The 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 of displacements vanishes. That identity, together with the fact that the once-around loop has winding 1, supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
A singular 2-simplex here is simply a continuous map from the standard topological 2-simplex $\Delta^2=\mathrm{stdSimplex},\mathbb{R}(\mathrm{Fin},3)$ into $S^1$ (the carrier of Mathlib's TopCat.sphere 1). The auxiliary map twoSimplexCoordOneParam extracts the middle barycentric coordinate $x_1\in I$ continuously; composing a path $\gamma:I\to S^1$ with that coordinate yields a map $\Delta^2\to S^1$.
Geometrically this is the triangular backtrack prism: the three faces of $F_\gamma$ are forced to be the reverse of $\gamma$, the constant path at $\gamma(0)$, and $\gamma$ itself. That face pattern is exactly what later cancels in the alternating boundary sum.
proof idea
One-line structure definition. The underlying function is $\gamma\circ\mathrm{twoSimplexCoordOneParam}$. Continuity is the composition of $\gamma$'s continuity with the already-proved continuity of the middle-coordinate projection on $\Delta^2$. No further algebraic or homotopy work occurs at this stage.
why it matters
This map is the geometric engine behind the chain-level backtrack 2-simplex. Downstream face lemmas identify its three faces with the reverse path, the constant initial edge, and the original path; pathBacktrackSingularTwoSimplex packages it as a singular 2-simplex in the homology complex.
Those faces feed the telescoping argument in the module doc: the boundary walk along two edges is homotopic rel endpoints (inside the convex, simply connected $\Delta^2$) to the direct edge, so displacement additivity plus homotopy invariance force the alternating face sum to vanish. That is the "winding kills boundaries" identity needed for the winding homomorphism on 1-cycles.
In the broader Recognition foundation this is pure classical topology scaffolding for $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$; it does not yet touch the forcing chain T0–T8, the J-cost, or the eight-tick octave. It closes no open RS physics claim, but it is a necessary step toward a fully formal singular-homology comparison on the circle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.