coneBaseParam_coe_of_coord_two_ne_one
plain-language theorem explainer
Away from the apex of the standard 2-simplex, the cone base parameter equals the normalized barycentric ratio x₁/(1−x₂). Anyone assembling the zero-winding cone filler for singular 1-simplices on S¹ cites this identity. The proof is a one-line simp that unfolds the piecewise definition under the non-apex hypothesis.
Claim. For every point $x$ of the standard $2$-simplex $\Delta^2\subset\mathbb{R}^3$, if the third barycentric coordinate satisfies $x_2\neq 1$, then the real value of the cone base parameter at $x$ equals $x_1/(1-x_2)$.
background
The module lifts path-level winding on $S^1$ to singular simplices and proves that displacement kills boundaries: for every singular $2$-simplex the alternating face sum of displacements vanishes. That identity is the chain-level half of the split injection $H_1(S^1;\mathbb{Z})\hookrightarrow\mathbb{Z}$.
The cone construction fills a closed edge by coning over the apex $v_2$ of $\Delta^2$. The barycentric base parameter records the normalized position along the base edge $v_0\to v_1$: away from the apex it is $x_1/(1-x_2)$, and at the apex it is set to $0$ so that later multiplication by $1-x_2$ restores continuity. The value lives in the unit interval $I$ and is fed into the canonical path lift of the closed edge.
Upstream, pathLift is the continuous real lift of a path on the circle cover; the cone angle is built by scaling that lift by the height $1-x_2$.
proof idea
One-line wrapper. Unfold the piecewise definition of the cone base parameter and discharge the if branch with the hypothesis $x_2\neq 1$; simp then reduces the subtype coercion to the explicit quotient $x_1/(1-x_2)$.
why it matters
This is the computational engine for every face-restriction identity of the cone parameter. Downstream it is rewritten into: base-face evaluation (parameter recovers the original $\Delta^1$ coordinate), side-face $\delta_0$ evaluation (parameter $=1$, terminal endpoint), side-face $\delta_1$ evaluation (parameter $=0$, initial endpoint), and non-apex continuity of the real-valued parameter. Those four facts let the lifted cone angle, and then the pointwise circle cone, be checked on faces and away from the apex, which is the remaining step toward a continuous zero-winding $2$-simplex filler. In the broader chain this supports the kills-boundaries identity that makes simplex displacement a homology invariant, completing the left-inverse 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.