A continuum whose hyperspace of regular subcontinua is homeomorphic to the irrationals

For a metric continuum X, let D(X) be the hyperspace of subcontinua of X equal to the closure of their interior, with the Hausdorff metric. Camargo, Ordoñez and Ramírez asked whether D(X) can be homeomorphic to the rationals or to the irrationals (Appl. Gen. Topol. 25 (2024), Question 3.26). We answer the latter question affirmatively. We construct a continuum X ⊆ ℓ² as the closure of a countable tree of scaled copies of an indecomposable plane continuum. Two types of piece alternate: blocks with dense interior, and spines with empty interior carrying densely attached blocks. We characterize all regular subcontinua by nonempty convex sets of pieces satisfying a density condition, and prove that this coding is a homeomorphism onto a Gδ subset of a Cantor cube. We then show that no point of D(X) has a compact neighborhood. The Alexandrov–Urysohn characterization yields D(X) ≅ ℕℕ, and hence D(X) is homeomorphic to the irrationals. We also explain why this construction does not extend to the rational case, which remains open. Lean formalization. The deposit includes a Lean 4 / Mathlib formalization (Lean 4.35.0, Mathlib commit 6015dbb) of the combinatorial core of the proof. Using only Lean's standard axioms, it proves that the code space of admissible sets of pieces is a nonempty, zero-dimensional, Polish (Gδ) subspace of a Cantor cube in which every compact subset has empty interior. Theorem A in the form D(X) ≅ ℕℕ is then derived from two results stated as explicit hypotheses: the Alexandrov–Urysohn theorem and the geometric identification of D(X) with the code space (Theorem 4.6 and Proposition 5.2 of the paper). The development was also checked with leanchecker and the external type checker nanoda. Status. Preprint; no independent expert has yet verified the proofs. The paper was prepared with substantial AI assistance (Claude Opus 5.5, Anthropic); see the AI disclosure in the paper and AI_DISCLOSURE.md. The full first prompt is included in prompt/first-prompt.md.