coneBaseParam_faceMap_one_coe_of_not_apex
plain-language theorem explainer
On the side face δ₁ of Δ², away from the apex, the cone base parameter is identically 0. Builders of the zero-winding cone filler for singular 1-simplices on S¹ cite this as the initial-endpoint side of the lifted cone formula. The proof is a short rewrite: the non-apex formula plus the δ₁ coordinate identities force the normalized base coordinate to vanish.
Claim. For every $x \in \Delta^1$ with terminal barycentric coordinate $x_1 \neq 1$, the real value of the cone base parameter at $\delta_1(x) \in \Delta^2$ equals $0$.
background
This 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 sending the once-around loop to 1, supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
The cone base parameter on $\Delta^2$ is the barycentric coordinate along the base edge $v_0\to v_1$: away from the apex $x_2=1$ it is $x_1/(1-x_2)$, and at the apex it is set to 0. The eventual zero-winding cone filler feeds this parameter into a lifted edge path and multiplies by $1-x_2$ for continuity at the apex.
The face map $\delta_1:\Delta^1\to\Delta^2$ is the affine map induced by the coface. On that side face the middle coordinate vanishes ($x_1=0$) and the apex coordinate equals the terminal $\Delta^1$ coordinate.
proof idea
Apply the non-apex evaluation of the cone base parameter, which rewrites it as $x_1/(1-x_2)$ once $x_2\neq 1$. The first subgoal is the vanishing of that quotient: the $\delta_1$ face identity forces the middle coordinate to 0, so the quotient is 0 by simplification. The second subgoal discharges $x_2\neq 1$ on the image: the $\delta_1$ face identity identifies the apex coordinate with the terminal coordinate of the original $x$, which is $\neq 1$ by hypothesis.
why it matters
This pins the initial-endpoint side of the lifted cone formula used to fill closed zero-winding edges. Downstream, coneLiftAngle_faceMap_one uses it to show the lifted cone angle is constant on the whole $\delta_1$ side face (equal to the initial path lift), and coneLiftAngle_simplexEdge_one specializes that constancy to the edge parameterization. Those constancy facts are the algebraic bookkeeping that lets the cone filler stay at the initial lift value along $\delta_1$, which is required for the homotopy that proves displacement kills boundaries on singular 2-simplices. In the broader chain this supports the winding homomorphism on 1-cycles as a left inverse to the fundamental class, the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.