coneBaseParam
plain-language theorem explainer
Barycentric base parameter on the standard 2-simplex for coning a closed edge over the apex vertex. Away from the apex it is the normalized base-edge coordinate x₁/(1−x₂); at the apex it is set to 0. Cited by the singular cone filler and face-restriction lemmas that prove winding kills boundaries on S¹. The body is a case split plus an interval-membership proof via barycentric sum and nonnegativity.
Claim. For $x$ in the standard $2$-simplex $\Delta^2=\mathrm{stdSimplex}\,\mathbb{R}\,(\mathrm{Fin}\,3)$, the cone base parameter is the point of the unit interval $I$ equal to $0$ when the apex coordinate satisfies $x_2=1$, and equal to $x_1/(1-x_2)$ otherwise (which lies in $[0,1]$ by barycentric nonnegativity and $x_0+x_1+x_2=1$).
background
The module lifts path-level winding on $S^1$ to singular simplices and proves that displacement vanishes on boundaries of singular $2$-simplices. That identity is the chain-level fact making winding a homology invariant, and half of the comparison $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
Coning a closed edge over an apex needs a continuous way to read a base-edge parameter off each point of $\Delta^2$. The standard $2$-simplex consists of $(x_0,x_1,x_2)$ with $x_i\ge 0$ and sum $1$. The apex is the vertex where $x_2=1$; the opposite face is the edge $v_0\to v_1$. Away from the apex the ray from the apex hits that edge at the normalized ratio $x_1/(1-x_2)$.
The unit interval $I$ is the codomain so the parameter can be fed into a lifted edge path. Multiplying the lift by the remaining height $1-x_2$ restores continuity at the apex in the eventual cone filler.
proof idea
Definition by cases on whether the apex coordinate equals $1$. At the apex return $0\in I$. Otherwise form the subtype $\langle x_1/(1-x_2),_\rangle$ and discharge membership in $I$ by: nonnegativity of $x_1$ from the simplex; strict inequality $x_2<1$ from $\le 1$ plus the case hypothesis; positivity of the denominator; then $x_1/(1-x_2)\le 1$ from the barycentric identity $x_0+x_1+x_2=1$ (via stdSimplex.sum_eq_one and Fin.sum_univ_three) together with $x_0\ge 0$ and linarith.
why it matters
This is the coordinate chart for the zero-winding singular cone used throughout CircleWindingChain. Downstream lemmas pin its values on faces: on the base face $\delta_2$ it recovers the original $\Delta^1$ coordinate; on side face $\delta_0$ (off apex) it is $1$; on $\delta_1$ (off apex) it is $0$; along the geometric base edge it is the unit-interval parameter. Those identities feed coneLiftAngle and the face-map computations that make the cone filler restrict correctly on the boundary walk.
Together with path-lift norm bounds (compactness input for apex continuity), this supports the telescoping proof that alternating face displacements sum to zero, i.e. winding kills boundaries. That is the homology-invariance half of the split injection of the fundamental class into $H_1(S^1)$. No Recognition forcing-chain step (T0–T8) is invoked here; the work is classical singular topology of the circle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.