faceMap_two_coord_one
plain-language theorem explainer
On the base face map δ₂ : Δ¹ → Δ², the second barycentric coordinate of any point is unchanged. Workers building cone parameters or restricting affine 2-simplices on S¹ cite this identity. The proof identifies δ₂ with castSucc and isolates the single nonzero summand in the barycentric pushforward.
Claim. For every point $x$ in the standard $1$-simplex $\Delta^1$, writing $y$ for its image under the topological face map induced by the coface $\delta_2 : [1]\to[2]$, the barycentric coordinate satisfies $y_1 = x_1$.
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}$.
Face maps here are the continuous affine maps $\Delta^1\to\Delta^2$ induced by the simplicial cofaces $\delta_i$. The $i$-th face of a singular $2$-simplex is composition with that map. Barycentric coordinates on $\mathrm{stdSimplex},\mathbb{R},(\mathrm{Fin},n)$ are the underlying functions $\mathrm{Fin},n\to\mathbb{R}$ summing to $1$.
The base face $\delta_2$ embeds $\Delta^1$ as the edge opposite vertex $2$. The cone parameter $x_1/(1-x_2)$ on $\Delta^2$ needs exactly the coordinate identity proved here: on that face, coordinate $1$ is preserved (and coordinate $2$ vanishes).
proof idea
Unfold the face map to $\mathrm{stdSimplex.map}$ of the concrete coface $\delta_2$. Identify that vertex map $\mathrm{Fin},2\to\mathrm{Fin},3$ with $j\mapsto j.\mathrm{castSucc}$ by exhaustive check on the two indices. After applying the finite-support linear-map evaluation, the image coordinate at $1$ is a sum over preimages. Only the summand at source index $1$ survives ($\mathrm{castSucc},1=1$); the other index is ruled out by a one-line $\mathrm{fin_cases}$, and the missing-index side condition is vacuous. Hence the sum equals $x_1$.
why it matters
This is a local coordinate lemma inside the singular-simplex winding package, not a Recognition forcing step (T0–T8). It is required wherever the base face of an affine or cone $2$-simplex must match a geodesic or interval parameter.
Downstream: it feeds the cone-base identity (on $\delta_2$ the cone parameter equals the original $\Delta^1$ coordinate), the statement that the $\delta_2$ face of the lift-affine $2$-simplex is the geodesic from $p$ to $q$, and the reparameterisation of coordinate-$1$ on that face to the unit interval. Those facts close the telescoping argument that displacement of alternating faces vanishes, i.e. winding is a homology invariant.
No open scaffold remains here; the declaration is fully proved and axiom-free.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.