coneBaseParam_faceMap_zero_coe_of_not_apex
plain-language theorem explainer
On the δ₀ face of the standard 2-simplex, away from the apex, the barycentric cone base parameter equals 1. Builders of the zero-winding cone filler and the lifted cone-angle formulas cite this to pin the terminal-endpoint side of a closed edge. The proof collapses the normalized ratio via face-map coordinate identities and the simplex sum-to-one constraint.
Claim. Let $x \in \Delta^1$ with barycentric coordinates $(x_0,x_1)$ and $x_1 \neq 1$. Writing $\delta_0:\Delta^1\to\Delta^2$ for the $0$-th face map, the real value of the cone base parameter at $\delta_0(x)$ equals $1$.
background
The module lifts path-level winding on $S^1$ to singular simplices and proves that simplex displacement kills boundaries: for every singular $2$-simplex the alternating face sum of displacements vanishes. That identity is the chain-level half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
The cone base parameter is the barycentric coordinate along the base edge $v_0\to v_1$ when coning a closed edge over the apex $v_2$. Away from the apex it equals $x_1/(1-x_2)$; at the apex it is set to $0$. The topological face map $\delta_0:\Delta^1\to\Delta^2$ embeds the $1$-simplex as the side opposite vertex $0$, with image coordinates $(\delta_0 x)_1=x_0$ and $(\delta_0 x)_2=x_1$.
Upstream, the coe lemma records that whenever the apex coordinate is not $1$, the cone base parameter is exactly that normalized ratio. The face-map coordinate lemmas identify those image coordinates with the original $\Delta^1$ barycentrics.
proof idea
Apply the coe lemma under the side condition that the image apex coordinate differs from $1$. That condition is the given $x_1\neq 1$ after rewriting via the face-map identity for coordinate $2$. The goal reduces to $x_0/(1-x_1)=1$. Sum-to-one on $\Delta^1$ (via the two-point Fin sum) yields $x_0+x_1=1$, hence $x_0=1-x_1$, and the ratio collapses by division by a nonzero quantity.
why it matters
Feeds three cone-lift formulas on the $\delta_0$ side: the general face formula for the lifted cone angle, its constant-on-face specialization when lifted endpoints agree, and the matching statement along the geometric edge. Those results assemble the zero-winding cone filler used in the telescoping argument that simplex displacement kills boundaries.
In the module program this is a coordinate pin: on $\delta_0$, away from the apex, the cone samples the terminal endpoint of the original closed edge. Paired with the $\delta_1$ statement (base parameter $0$, initial endpoint), the cone interpolates correctly between the two lifts. The larger goal is the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ via winding; the generation half still needs a simplicial prism or subdivision operator that Mathlib singular homology does not yet supply.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.