coneBaseParam_faceMap_two_coe
plain-language theorem explainer
On the base face δ₂ of the standard 2-simplex, the cone base parameter collapses to the original Δ¹ barycentric coordinate x₁. Anyone building the zero-winding cone filler or comparing lifted angles on δ₂ cites this identity. The proof rewrites via the off-apex formula, substitutes the face-map coordinate identities x₂=0 and x₁ preserved, and finishes by ring/norm_num.
Claim. For every point $x$ of the standard $1$-simplex $\Delta^1=\mathrm{stdSimplex}\,\mathbb{R}\,(\mathrm{Fin}\,2)$, the real value of the cone base parameter at the image of $x$ under the topological face map $\delta_2:\Delta^1\to\Delta^2$ equals the second barycentric coordinate $x_1$ of $x$.
background
The module lifts path-level winding on $S^1$ to singular simplices and proves the chain-level identity 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 telescoping uses a continuous cone filler over the apex $v_2$.
The cone base parameter on $\Delta^2$ is the normalized barycentric coordinate along the base edge $v_0\to v_1$: away from the apex it is $x_1/(1-x_2)$, and at $x_2=1$ it is set to $0$. The face map $\delta_2:\Delta^1\to\Delta^2$ is the affine coface embedding of the geometric base face. On that face the coordinate identities are $x_2=0$ and the middle coordinate preserved: $(\delta_2 x)_1=x_1$.
Upstream, coneBaseParam_coe_of_coord_two_ne_one records the off-apex formula, while faceMap_two_coord_one and faceMap_two_coord_two supply the two barycentric identities used here.
proof idea
Term-mode rewrite proof. First apply the off-apex evaluation of the cone base parameter, which requires $x_2\neq 1$ on the image point. The main goal becomes $x_1/(1-x_2)=x_1$ after substituting the face-map coordinates; rewrite with the identities $(\delta_2 x)_1=x_1$ and $(\delta_2 x)_2=0$, then close by ring. The side goal $x_2\neq 1$ is the same face identity $(\delta_2 x)_2=0$, discharged by norm_num.
why it matters
This is the coordinate reduction that makes the cone filler agree with the original edge path on the whole base face $\delta_2$, not merely on the geometric edge. Downstream it feeds coneBaseParam_simplexEdge_two_coe (parameter equals the unit-interval coordinate along $v_0\to v_1$), and the two lifted-angle comparisons coneLiftAngle_faceMap_two and coneLiftAngle_faceMap_two_of_oneSimplex, which state that on $\delta_2$ the lifted cone angle equals the path lift after the standard $\Delta^1\simeq I$ reparameterisation.
Those comparisons are ingredients of the $2$-simplex telescoping that proves displacement kills boundaries, the chain-level fact giving the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ together with the once-around generator evaluation. In the Recognition foundation stack this is pure singular-homology scaffolding for the circle, not a forcing-chain (T0–T8) step; it closes a concrete algebraic identity inside the winding-invariant development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.