The route is Toruńczyk’s characterisation: a Polish absolute retract with the discrete approximation property is homeomorphic to ℓ². Ishiki establishes the two substantive halves separately — the absolute retract property in Parts I–III, by building continuous invariant full-support measures, turning them into finite-dimensional local models in which every isometry group acts through one fixed O(n), and passing to the orbit space of a hyperspace; and the discrete approximation property in Part IV, by a construction independent of the first three.
Write 𝕄₁ = {(X,d) ∈ 𝕄 : diam(X,d) = 1}, and write • for the one-point space. Four steps, none of them new, and all of them cheap.
1. 𝕄₁ is Polish. The diameter is continuous on 𝕄, since |diam X − diam Y| ≤ 2·𝒜𝒥(X,Y). So 𝕄₁ is a closed subspace of a Polish space.
2. The complement of a point splits. • is the unique element of diameter zero, and rescaling is continuous for 𝒜𝒥, so
3. Removing a point from ℓ² changes nothing. By Ishiki’s theorem 𝕄 ≅ ℓ², and ℓ² ∖ {0} ≅ ℓ² by Bessaga–Klee. Hence 𝕄 ∖ {•} ≅ ℓ², and with step 2,
4. 𝕄₁ is an absolute retract. Rescaling to diameter one retracts 𝕄 ∖ {•} onto 𝕄₁, and a retract of an absolute retract is an absolute retract. So the expensive half of Toruńczyk’s hypothesis — the half that cost Ishiki three of his four parts — comes for free on the slice.
What is not free is the other half.
𝕄₁ has the discrete approximation property: for every sequence of compact metrizable Kᵢ, continuous fᵢ : Kᵢ → 𝕄₁ and open cover 𝒰 of 𝕄₁, there are continuous gᵢ, each 𝒰-close to fᵢ, whose images form a discrete family.
Ishiki’s Theorem 14.1 separates images by a construction with a scale-free invariant at its centre: multiply by a short interval and a small finite equilateral space, raise the product distances to distinct powers, then distinguish the results by the Hausdorff dimensions of their connected subsets, and increase the cardinalities of the finite factors to stop the images accumulating. Hausdorff dimension is invariant under rescaling. Renormalising every constructed space to diameter one therefore leaves the separating invariant untouched, and the cardinality argument is combinatorial and unaffected. What has to be checked is that the two controlled perturbations — the short interval and the finite equilateral factor — can be chosen so that the renormalised spaces stay within the prescribed cover, which is a statement about how much the diameter moves under those perturbations, not about the separation.
Step 3 gives 𝕄₁ × ℝ ≅ ℓ². That does not give 𝕄₁ ≅ ℓ². Factor problems in infinite-dimensional topology are not formalities, and a Polish absolute retract whose product with a line is ℓ² is not thereby ℓ² on any theorem quoted in this note. Anyone reading steps 1–4 as a proof has taken the one step the note exists to refuse. The content of WP-108 is precisely that the gap is a single named property and not a vague remainder.
Ishiki’s Questions 15.2 and 15.5 — whether the Nakajima–Shioya compactification of 𝕄, and whether the pyramid space Π under the weak topology, are homeomorphic to the Hilbert cube — are one question asked twice. Both reduce to Toruńczyk’s cube characterisation: compact, metrizable, absolute retract, disjoint cells property. For Π the literature supplies contractible and locally path connected, which is short of an absolute retract, so each is the same two-step: upgrade to AR, then verify DDP. Questions 15.3 and 15.4 are of a different kind and are harder: they ask for contractions of 𝒜𝒥 balls, and Corollary 14.4 explicitly declines to prescribe its neighbourhoods as balls. A homeomorphism to ℓ² destroys the metric, so those two are not corollaries of the main theorem at all.
Nothing in this note is machine-checked and nothing in it should be cited as verified. Toruńczyk’s characterisation, Bessaga–Klee, and the absolute retract calculus are quoted from the literature; the corpus has no formalisation of any of them and Mathlib has no infinite-dimensional topology of this kind. The one part of Ishiki’s paper that would be a plausible formalisation target is unrelated to this question: Remark 14.5 identifies the non-Archimedean Gromov–Hausdorff space isometrically with an explicit ultrametric function space, which is concrete in a way nothing else here is.
| Ishiki 2026 | Y. Ishiki, The topology of Gromov–Hausdorff space, arXiv:2609.09639v2, 10 Sep 2026. Theorem 1.1; Theorem 14.1; Corollary 14.4; Remark 14.5; §15 Questions. |
| Toruńczyk 1981 | Characterizing Hilbert space topology. Fund. Math. 111, 247–262; with the correction noted in Ishiki §1. |
| Bessaga–Klee | Removal of a point from an infinite-dimensional Fréchet space does not change its topology. |
| Antonyan 2020, 2021 | The Gromov–Hausdorff hyperspace of a Euclidean space I and II. Adv. Math. 363, 106977; 393, 108055. The questions Ishiki’s Theorem 1.1 answers. |
| Kazukawa–Nakajima–Shioya | Contractibility and local path connectedness for the box and concentration topologies; (𝒳, dconc) is not Baire. |
| Internal | WP-82 · The Missing Floor · Book 7 · Beltrami · Vol XIII Ch 9 |