Choquet Simplex

A metrizable Choquet simplex is a nonempty compact set in a real topological vector space with a locally convex topology satisfying the Hausdorff axioms, such that is a convex set and each has a unique representing probability measure on its Borel sigma-algebra concentrated on its extreme points. Here metrizability means that the topology is induced by a metric. If denotes the set of extreme points, the representing measure satisfies

(1)

where is any continuous function on that preserves convex combinations. Such representing measures exist for every metrizable compact set that is also a convex set, but their uniqueness is an additional condition (Phelps 2001). This characterization is stated for the metrizable case.

Every finite-dimensional simplex has this property, since each point has unique weights in its convex combination of the polytope vertices. A square does not, since its center is the midpoint of either pair of opposite polytope vertices. The Poulsen simplex is an infinite-dimensional example whose extreme points form a dense set.

For a nonempty separable space with a metric bounded by 1, choose a countable set that is also a dense set in , and let be the set closure of the convex hull of the distance profiles in the product space . Sabok (2016, Question 9.4) asked whether this construction always gives a Choquet simplex and whether the corresponding construction for the Urysohn sphere gives the Poulsen simplex.

Zhang and Yang (2026a) reported negative answers to both questions. Their finite example is the cycle graph with its graph distance divided by 2. Its scaled graph distance matrix is

(2)

The four row vectors , , , and are the polytope vertices of a parallelogram and satisfy

(3)

The two pairs therefore give distinct representing probability measures for the same point. Their Urysohn sphere argument also constructs distinct representing probability measures, but requires the full infinite-coordinate space rather than just this finite example.

The authors used GPT-based models to develop proof strategies and selected Lean components. As of Oct. 2, 2026, the Lean development verified finite and metric obstruction arguments, but did not formalize the complete identification of or the final Choquet and Poulsen simplex conclusions. Independent specialist review of the complete arguments had not been reported (Zhang and Yang 2026b, VibeMathed 2026).