Finite and Urysohn obstructions to Sabok's S-prime simplex questions
Yutong Zhang, Yaoran Yang
math.MG
Jun 18, 2026 · v1
math.CO math.FA
TL;DR
Selected proof components, developed with the CSSC framework and GPT assistance, were formalized in Lean 4; the development is in a public repository.
Abstract
Sabok asked whether the compact convex set \(S'(X)\) attached to a separable metric space of diameter at most one is always a simplex, and whether \(S'(\mathbb U_1)\) is the Poulsen simplex. We give negative answers. For finite \(X=\{x_1,\ldots,x_m\}\), \(S'(X)\) is affinely homeomorphic to the convex hull of the rows \(r_i=(d(x_i,x_1),\ldots,d(x_i,x_m))\) of the distance matrix; it is a simplex exactly when these rows are affinely independent. The diameter-one four-cycle gives the minimal finite obstruction. For the Urysohn sphere, using the rational Urysohn sphere \(D\) as coordinates, we identify the coordinate model \(S'_D(\mathbb U_1)\) with the Katétov compactum \(K(D)\). Four explicit extreme points \(f_A,g_A,\mathbf 1,\mathbf h\) satisfy \(f_A+g_A=\mathbf 1+\mathbf h\), giving two distinct representing measures for \((3/4)\mathbf 1\). Hence \(S'(\mathbb U_1)\) is not a Choquet simplex.
Problem
Sabok asked whether the compact convex set S'(X), attached to a separable metric space of diameter at most one, is always a simplex. He also asked whether S'(U_1) for the Urysohn sphere is the Poulsen simplex.
Approach
For finite X, S'(X) is identified with the convex hull of the rows of the distance matrix. It is a simplex exactly when those rows are affinely independent, and the diameter-one four-cycle gives a minimal counterexample. For the Urysohn sphere, S'_D(U_1) with rational Urysohn coordinates is identified with the Katětov compactum K(D). Four explicit extreme points are then constructed. Selected proof components were formalized in Lean 4.
Results
Both questions are answered negatively. The extreme points satisfy f_A + g_A = 1 + h, so (3/4)·1 has two distinct representing measures. Hence S'(U_1) is not a Choquet simplex and not the Poulsen simplex.
