faceMap_two_coord_two
plain-language theorem explainer
On the base face map δ₂ : Δ¹ → Δ², every point has vanishing third barycentric coordinate. Anyone computing cone parameters or edge lifts on the standard 2-simplex cites this coordinate identity. The proof reduces the coface to cast-successor and shows the preimage of vertex 2 is empty, so the pushforward mass at index 2 is zero.
Claim. For every point $x$ of the standard $1$-simplex $\Delta^1 = \mathrm{stdSimplex}\,\mathbb{R}\,(\mathrm{Fin}\,2)$, the image under the topological face map induced by the coface $\delta_2 : [1] \to [2]$ has third barycentric coordinate equal to zero: $(\delta_2(x))_2 = 0$ in $\Delta^2$.
background
The module lifts path winding on $S^1$ to singular simplices and proves that displacement kills boundaries: for any 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}$.
Here $\mathrm{faceMap},i$ is the continuous affine map $\Delta^1 \to \Delta^2$ induced by the simplicial coface $\delta i : [1] \to [2]$. Faces of a singular $2$-simplex are compositions $F \circ \mathrm{faceMap},i$. Barycentric coordinates on $\Delta^n$ are the standard nonnegative weights summing to $1$ indexed by $\mathrm{Fin},(n+1)$.
The base face $\delta_2$ embeds $\Delta^1$ as the edge opposite vertex $2$, so the cone (height) coordinate along that face must vanish. Upstream, faceMap_apply identifies the map with stdSimplex.map of the concrete coface homomorphism.
proof idea
Rewrite via faceMap_apply, then work with the underlying FunOnFinite.linearMap of the coface. Prove by fin_cases that the concrete map of $\delta_2$ equals cast-successor $\mathrm{Fin},2 \to \mathrm{Fin},3$ (so $0 \mapsto 0$, $1 \mapsto 1$). After FunOnFinite.linearMap_apply_apply, coordinate $2$ is a sum of $x$-masses over the preimage of $2$; that preimage is empty, so the sum is zero by Finset.sum_eq_zero.
why it matters
This is the coordinate fact that makes the base face of the cone genuinely flat. Downstream it feeds coneBaseParam_faceMap_two_coe (cone base parameter recovers the original $\Delta^1$ coordinate), the family coneLiftAngle_faceMap_two, coneLiftAngle_faceMap_two_of_oneSimplex, and coneLiftAngle_simplexEdge_two (lifted cone angle agrees with the path lift on $\delta_2$), and linearTwoSimplexMap_face_two (the $\delta_2$ face of the lift-affine $2$-simplex is the geodesic from $p$ to $q$).
Those cone-lift identities are the geometric engine behind the $2$-simplex telescoping that proves simplexDisplacement_boundary. In the module's program that is the chain-level "winding kills boundaries" step toward a left inverse to the fundamental class on $H_1(S^1)$. It is pure singular-simplex geometry; no Recognition forcing-chain step (T0–T8) is invoked here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.