continuousAt_coneBaseParam_of_coord_two_ne_one
plain-language theorem explainer
Away from the apex of the standard 2-simplex, the barycentric cone base parameter is continuous as an I-valued map, not merely after real coercion. Builders of the zero-winding cone filler for singular 2-simplices on S¹ cite this. The proof is a short subtype-range wrapper around the already-proved real-valued continuity at non-apex points.
Claim. For every point $x$ in the standard $2$-simplex $\Delta^2\subset\mathbb{R}^3$ with third barycentric coordinate $x_2\neq 1$, the cone base parameter (normalized base-edge coordinate $x_1/(1-x_2)$, valued in the unit interval $I$) is continuous at $x$ as an $I$-valued map.
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$, 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 base parameter is the barycentric coordinate used when coning a closed edge over the apex $v_2$ of $\Delta^2$. Off the apex it equals $x_1/(1-x_2)$ (normalized position along the base edge $v_0\to v_1$); 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$ to restore continuity at the apex.
An upstream result already gives continuity of the real-valued (coerced) parameter away from $x_2=1$. The present statement upgrades that to continuity into the subtype $I=[0,1]$.
proof idea
Unfold continuity at a point, then rewrite via the characterization of continuity into a subtype: a map into a subtype is continuous at $x$ precisely when the coerced real-valued map is. Discharge the goal by the upstream theorem that the real-valued cone base parameter is continuous at every non-apex point. No new analysis is performed; the argument is a one-line subtype-range wrapper.
why it matters
The immediate consumer is continuity of the lifted cone angle away from the apex: that theorem unfolds the angle formula and invokes this result to obtain continuity of the base parameter before composing with the continuous path lift. Together those facts assemble the continuous cone filler used in the $2$-simplex telescoping argument behind the kills-boundaries identity.
In the broader Recognition foundation 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}$). The generation/surjectivity half still needs a simplicial prism or subdivision operator that Mathlib singular homology does not yet supply; the present lemma is pure continuity scaffolding inside the already-proved injective half.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.