On the structure of countable hyperspaces of regular subcontinua

Main result. If X is a metric continuum whose hyperspace D(X) of regular subcontinua is countable, then D(X) is a Gδ subset of C(X), hence completely metrizable and scattered, with dense isolated points. In particular D(X) is never homeomorphic to the rationals. This answers the rational case of a question of Ramírez Angarita (2023, Pregunta 3.2.14) and of Camargo, Ordoñez and Ramírez (Appl. Gen. Topol. 25 (2024), Question 3.26); the irrational case was answered in the companion repository. Every theorem of the paper is formalized in Lean 4 with Mathlib