Characterization of the contiguous subsets of the reals

Non-blind read-back — not independent testimony. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statements, with full knowledge of the source text and of the intended meaning. It was not produced by a blind, independent auditor, so it must not be mistaken for independent testimony; reviewers should compare the Lean code against the source themselves.

Order notions. For a (pre)ordered set $Q$: $Q$ is sparse if every closed interval $[a,b]=\{q: a\le q\le b\}$ is finite; $Q$ is dense (book sense) if $[a,b]$ is infinite whenever $a<b$; $A\subseteq Q$ is a dense subset if for all $q_1<q_2$ there is $q\in A$ with $q_1\le q\le q_2$; $Q$ is complete if every nonempty subset that is bounded above has a least upper bound in $Q$. A linear order $\preceq$ on $X$ is a natural order if the order topology of $\preceq$ (generated by all rays $\{x: a\prec x\}$ and $\{x: x\prec b\}$) equals the natural topology $\mathcal T$. $D$ is fully characterized by a topological space $Q$ if there is a homeomorphism $(X,\mathcal T)\to Q$. "Decidable" means $\Omega\setminus s\in\mathcal D$ for all $s\in\mathcal D$.

Statement. For every linearly ordered type $Q$, the conjunction of (i) $[a,b]$ is infinite for all $a<b$, (ii) every nonempty subset of $Q$ bounded above has a least upper bound in $Q$, and (iii) there is a countable $A\subseteq Q$ such that for all $q_1<q_2$ some $q\in A$ satisfies $q_1\le q\le q_2$, holds if and only if there is an order-connected $S\subseteq\mathbb R$ and an order isomorphism $Q\cong S$. ($S$ may be empty, a point, or any interval.)