{"id":"palomar/PALOMAR-2026-09-28-000004","url":"https://github.com/yoshito-ishiki-math/lean-gh-space-hilbert/tree/8b25d3fc5b9f2a61dffa59e1daa8c9c483f70a46","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-28-000004-v1.json","repo":"https://github.com/yoshito-ishiki-math/lean-gh-space-hilbert","tags":["math.GN","math.MG","msc:54E35","msc:54C55","lean","metric-geometry","gromov-hausdorff","topology"],"score":0,"title":"Conditional Hilbert-space classification of Gromov--Hausdorff space","trust":"high","domain":"math.GN","source":"palomar","authors":["Yoshito Ishiki"],"reviews":0,"subject":"math.GN","summary":"A Lean formalization of the implication from five explicitly stated literature inputs to a homeomorphism between the ordinary Gromov--Hausdorff space of nonempty compact metric spaces and real square-summable sequences. The proof constructs invariant full-support probability assignments, finite dimensional local models, global AR domination and discrete approximation. The five literature inputs are assumptions, not theorems proved in this snapshot.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-28","reactions":{},"formalized":true,"formalizes":[{"title":"The topology of Gromov--Hausdorff space","identifier":"arxiv:2609.09639v4","relationship":"formalizes"}]}