coneBaseParam_simplexEdge_two_coe
plain-language theorem explainer
Along the geometric base edge v₀→v₁ of the standard 2-simplex, the barycentric cone base parameter equals the unit-interval coordinate t. Anyone building the zero-winding cone filler or checking that the lifted cone angle restricts to the original path lift cites this. The proof is three successive rewrites through the face-map and interval reparameterisation.
Claim. For every $t \in I = [0,1]$, if $e_2(t)$ denotes the geometric base edge of $\Delta^2$ (the image of $t$ under the face map $\delta_2$ composed with the affine map $I \to \Delta^1$), then the real value of the cone base parameter at $e_2(t)$ equals $t$.
background
The 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 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 over the apex $v_2$ of $\Delta^2$. The cone base parameter is the barycentric quantity that, away from the apex, equals $x_1/(1-x_2)$ (normalized coordinate along $v_0 \to v_1$) and is set to $0$ at the apex. The geometric edge selected by face index $2$ is $\delta_2$ composed with the affine reparameterisation $t \mapsto (1-t,t)$ of $\Delta^1$.
Upstream, the face-map restriction already shows that on the abstract base face the cone parameter recovers the second barycentric coordinate of $\Delta^1$, and that coordinate is exactly $t$ under the interval-to-simplex map.
proof idea
One-line rewrite chain. Unfold the geometric edge as face map composed with interval-to-simplex; apply the already-proved identity that the cone base parameter on the base face $\delta_2$ equals the $\Delta^1$ coordinate $x_1$; finish by the definitional fact that the second barycentric coordinate of the interval-to-simplex map is $t$ itself.
why it matters
Feeds directly into the restriction theorem for the lifted cone angle: on the base edge, the cone lift equals the original path lift. That restriction is the continuity/endpoint check needed so the cone filler has zero winding and can serve as a singular 2-chain witnessing that a closed edge bounds when its displacement vanishes.
In the broader module this is scaffolding for the kills-boundaries identity (the 2-simplex telescoping that yields $\mathrm{disp}(\delta_1 F) = \mathrm{disp}(\delta_2 F) + \mathrm{disp}(\delta_0 F)$). Together with the fundamental-loop normalisation, that identity supplies the left-inverse half of $H_1(S^1;\mathbb{Z}) \cong \mathbb{Z}$. The generation/surjectivity half still waits on a simplicial prism or subdivision operator absent from Mathlib's singular homology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.