twoSimplexCoordOneParam_face_zero
plain-language theorem explainer
On the coface δ₀ : Δ¹ → Δ², the second barycentric coordinate of the image equals the reversed unit-interval parameter of the source 1-simplex. Anyone building the triangular backtrack prism for path winding cites this face identity. The proof is a short coordinate chase: faceMap_zero_coord_one plus the sum-to-one relation on Δ¹, finished by linarith.
Claim. For every $x \in \Delta^1$, the unit-interval parameter given by the second barycentric coordinate of $\delta_0(x) \in \Delta^2$ equals the reverse $t \mapsto 1-t$ of the standard homeomorphism $\Delta^1 \simeq I$ applied to $x$. Equivalently, $(\delta_0 x)_1 = 1 - x_1$.
background
The module lifts path-level winding on $S^1$ to singular simplices and proves that simplex displacement kills boundaries, the chain-level fact behind the split injection $\mathbb{Z} \hookrightarrow H_1(S^1;\mathbb{Z})$.
Here $\mathrm{faceMap}, i$ is the continuous affine map $\Delta^1 \to \Delta^2$ induced by the $i$-th coface $\delta i : [1] \to [2]$. The auxiliary map $\mathrm{twoSimplexCoordOneParam}$ reads the second barycentric coordinate of a point of $\Delta^2$ as an element of the unit interval $I$. The homeomorphism $\mathrm{stdSimplexHomeomorphUnitInterval}$ identifies $\Delta^1$ with $I$ by sending $x$ to its second coordinate $x_1$.
Upstream, $\mathrm{faceMap_zero_coord_one}$ records that on the side face $\delta_0$, the $\Delta^2$-coordinate of index $1$ equals the initial barycentric coordinate $x_0$ of the source $\Delta^1$. Combined with $x_0+x_1=1$ on the standard $1$-simplex, this forces the reversed-interval identity used below.
proof idea
Pointwise equality of continuous maps $I \to \mathbb{R}$ is enough, so ext reduces to a real equality of coordinates. Unfold the definitions: the left side is the second barycentric coordinate of $\delta_0 x$, the right side is $1$ minus the real value of the $\Delta^1\simeq I$ homeomorphism. Rewrite the homeomorphism via stdSimplexHomeomorphUnitInterval_coe (value equals $x_1$) and the face via faceMap_zero_coord_one (value equals $x_0$). The remaining identity $x_0 = 1-x_1$ is the sum-to-one relation on $\Delta^1$ (stdSimplex.sum_eq_one specialized to Fin 2), discharged by linarith.
why it matters
This is the face-$0$ coordinate lemma for the triangular backtrack prism. Downstream, pathBacktrackMap_face_zero applies it directly: the $0$-face of the prism over a path $\gamma$ is the singular $1$-simplex of the reversed path. That prism is the geometric engine of the module's kills-boundaries identity (simplexDisplacement_boundary): the three faces of the prism are the reversed path, a constant edge, and the original path, so alternating face displacements cancel.
In the broader Recognition foundation this supplies the chain-level half of the winding homomorphism that left-inverts the fundamental class of $S^1$, the split-injective side of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The generation/surjectivity half still needs a simplicial prism or subdivision operator not yet in Mathlib singular homology; this lemma is pure coordinate bookkeeping on that path.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.