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

This paper was prepared with substantial assistance from Claude Opus 5.5 (Anthropic). Most of the work was done jointly by the author and Claude. The author set the task, supplied the literature, gave the directions and provided feedback at each stage. Claude proposed the construction of Section~\ref{sec:construction}, wrote the proofs and produced the Lean formalization. The author proposed Question~3.26 of~\cite{CORa}, posed earlier in \cite[Pregunta~3.2.14]{Ra}, as the research target and gave a research plan: \begin{itemize} \item use the known restrictions on $\D(X)$ to rule out hopeless cases: $\D(X)$ compact only when finite, $\D(X)=\{X\}$ for indecomposable $X$, arcwise connected for locally connected $X$, never homeomorphic to $\N$; \item try the rational case through decomposable, inverse-limit or non-locally-connected constructions, and the irrational case through the classical characterization of the Baire space. \end{itemize} The manuscript then went through several rounds of feedback, each followed by a revision: \begin{enumerate} \item An audit of the first version found errors in a diameter estimate, a remark on a variant of the construction, an index in an example, and a planar realization. These were corrected and the proofs expanded. \item The author found that the core-protection conjecture of the first version is false: the continuum of \cite[Ejemplo~3.2.1]{Ra}, discussed in Section~\ref{subsec:nested}, violates it. The author then gave new directions: \begin{itemize} \item remove the conjecture and the claims about the rational case; \item instead, explain why the method does not apply to the rationals (Section~\ref{sec:rationals}); \item compare the text directly with the literature. \end{itemize} \item The author revised the manuscript. An audit, checked by the author and Claude Opus 5.5, then led to corrections of wording and citations. \item Later rounds of feedback from the author improved readability (figures and explanatory passages), completed the proof in Section~\ref{subsec:nested}, shortened Section~\ref{subsec:independent} and filled small gaps in the exposition. \end{enumerate} ChatGPT-Astra (OpenAI) was used, together with the author, to check successive versions of the manuscript and to send feedback. Claude formalized the combinatorial core of the proof in Lean~4 (version 4.35.0) with Mathlib (commit \texttt{6015dbb}). The Lean source accompanies this paper as supplementary material; it builds with \texttt{lake build}, and \texttt{lake env lean CheckAxioms.lean} lists the axioms used. Sets of pieces are encoded as points of the Cantor cube $\{0,1\}^{\Pc}$, where $\Pc$ is the tree of Section~\ref{subsec:tree} with its parent map; Lean indexes from $0$ rather than $1$, which only relabels the tree. Condition~(c) of Theorem~\ref{thm:description} is encoded without geometry: for a countable base $(V_j)$ of $K$, put $N_j=\{k:a_k\in V_j\}$; an included spine $S_{\beta,m}$ must have, for every $j$, infinitely many included children $B_{\beta^\frown(m,k)}$ with $k\in N_j$. This is equivalent to~(c) because $K$ has no isolated points and the points $a_k$ are distinct. Without \texttt{sorry} or added axioms, Lean proves that the code space of admissible sets is a nonempty, zero-dimensional $G_\delta$ subset of the Cantor cube, that it is Polish, and that each of its compact subsets has empty interior; these are the code-space counterparts of Propositions~\ref{prop:Gdelta} and~\ref{prop:nlc}. The statement $\D(X)\cong\N^\N$ of Theorem~\ref{thm:A} is then derived from two results that are not formalized and enter as explicit hypotheses rather than axioms: \begin{itemize} \item the Alexandrov--Urysohn theorem \cite[Theorem~7.7]{Ke}; \item the identification of $\D(X)$ with the code space (Theorem~\ref{thm:description} and Proposition~\ref{prop:homeo}), the geometric core of the paper, whose proof uses the Knaster continuum and composants. \end{itemize} The final step $\N^\N\cong\I$ (Fact~\ref{fact:polish}(c)) is classical and is not formalized. The file \texttt{SanityChecks.lean} checks the translation on small examples, and the development was also checked with the kernel replay tool \texttt{leanchecker} and with the independent type checker \texttt{nanoda}. No independent expert has yet verified the proofs. The author takes full responsibility for the content.