twoSimplexCoordOneParam_face_one
plain-language theorem explainer
On the middle face of the standard 2-simplex, the second barycentric coordinate vanishes for every point of Δ¹. Anyone tracking face restrictions of singular 2-simplices on S¹ cites this when identifying constant edges of backtrack prisms. The proof is a short reduction to the known coordinate identity for the coface map δ₁.
Claim. For every point $x$ of the standard $1$-simplex $\Delta^1$, the second barycentric coordinate of its image under the face embedding $\delta_1:\Delta^1\to\Delta^2$, read as a parameter in the unit interval $I$, equals $0$.
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$, the alternating face sum of displacements vanishes. That identity is the chain-level half of the split injection $H_1(S^1;\mathbb{Z})\hookrightarrow\mathbb{Z}$.
Face maps are the continuous affine maps $\Delta^1\to\Delta^2$ induced by the cofaces $\delta_i:,[1]\to,[2]$ of the simplex category. The middle face $\delta_1$ is the side opposite the middle vertex. The auxiliary map that reads the second barycentric coordinate of a point of $\Delta^2$ as a unit-interval parameter is the natural projection onto that coordinate (which lands in $I$ by the simplex inequalities).
Upstream, the coordinate identity already records that on $\delta_1(\Delta^1)$ the middle barycentric coordinate is identically zero. The present statement packages that fact in the unit-interval parameter language used by path-backtrack constructions.
proof idea
Pointwise equality of continuous maps $I\to\mathbb{R}$ is reduced by ext to equality of the underlying real values. Unfolding the parameter map turns the goal into the statement that the middle barycentric coordinate of $\delta_1(x)$ is $0$, which is exactly the upstream coordinate identity for the middle face map. The proof is therefore a one-line application of that identity after a change of presentation.
why it matters
The parent result is the face-one identity for the path-backtrack $2$-simplex: the middle face of the backtrack prism on a path $\gamma$ is the constant $1$-simplex at $\gamma(0)$. That identity is obtained by pushing the present vanishing through $\gamma$, so the parameter along the middle edge is constantly the start point.
In the broader module this is scaffolding for the telescoping argument that displacement kills boundaries on singular $2$-simplices (the chain-level half of the winding isomorphism $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$). It does not itself touch the Recognition forcing chain (T0–T8) or the J-cost; it is pure singular-homology infrastructure for the circle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.