[proofplan] We make the comparison precise by using regular Cauchy sequences, because their error terms are stable under the lower-cut construction. For a located Dedekind cut, the standard rational bisection theorem supplies inhabited families of small rational intervals; countable choice selects one interval at each precision, and interval overlap gives the Cauchy estimate for the selected midpoints. For a regular [Cauchy sequence](/page/Cauchy%20Sequence), the lower-cut definition gives a located Dedekind cut by direct rational estimates. The same estimates prove that reconstructing in either direction gives the original object, up to the stated equality relations. [/proofplan] [step:Choose small rational intervals around a located cut] Let $L \subset \mathbb{Q}$ be a located Dedekind cut. For each $n \in \mathbb{N}$, define $A_n(L)$ to be the set of pairs $(a,b) \in \mathbb{Q} \times \mathbb{Q}$ such that $a \in L$, $b \notin L$, and $0<b-a \leq 2^{-(n+2)}$. By the standard rational bisection theorem for located cuts, each $A_n(L)$ is inhabited. The index set is $\mathbb{N}$, so the assumed countable choice principle applies to the family $(A_n(L))_{n \in \mathbb{N}}$. Hence there is a sequence of rational pairs $((a_n,b_n))_{n \in \mathbb{N}}$ with $(a_n,b_n) \in A_n(L)$ for every $n$. Define the rational sequence $p: \mathbb{N} \to \mathbb{Q}$ by $p_n=(a_n+b_n)/2$. If $m,n \in \mathbb{N}$, then $a_m \leq b_n$ and $a_n \leq b_m$. Indeed, if $b_n<a_m$, then downward closure of $L$ and $a_m \in L$ imply $b_n \in L$, contradicting $b_n \notin L$. The [second inequality](/theorems/2136) is identical with $m$ and $n$ interchanged. Thus the intervals $[a_m,b_m]$ and $[a_n,b_n]$ overlap or touch. Since $p_m$ and $p_n$ are their midpoints, \begin{align*} |p_m-p_n| \leq (b_m-a_m)/2+(b_n-a_n)/2. \end{align*} Using the defining bounds on admissible intervals, \begin{align*} |p_m-p_n| \leq 2^{-(m+3)}+2^{-(n+3)} \leq 2^{-m}+2^{-n}. \end{align*} Therefore $p$ is a regular Cauchy real. [guided] We first isolate exactly where countable choice is used. For the fixed located cut $L$, and for each natural number $n$, let $A_n(L)$ be the set of rational intervals $(a,b)$ with $a \in L$, $b \notin L$, and $0<b-a \leq 2^{-(n+2)}$. The standard rational bisection theorem for located cuts says precisely that each of these sets is inhabited: locatedness lets us bisect a rational interval known to cross the cut, and after finitely many bisections we get a crossing interval of the requested rational length. Because the family is indexed by $\mathbb{N}$ and each member is inhabited, the stated countable choice principle gives a sequence $((a_n,b_n))_{n \in \mathbb{N}}$ with $(a_n,b_n) \in A_n(L)$ for all $n$. Now define $p_n=(a_n+b_n)/2$. The main point is not merely that each interval is short; different intervals must also be compatible because they cross the same cut. Let $m,n \in \mathbb{N}$. If $b_n<a_m$, then $a_m \in L$ and downward closure of $L$ force $b_n \in L$, contradicting $b_n \notin L$. Hence $a_m \leq b_n$. Interchanging $m$ and $n$ gives $a_n \leq b_m$. These two inequalities say that the two rational intervals overlap or at least touch. For two overlapping intervals, the distance between their midpoints is bounded by half the sum of their lengths. Applying this to $[a_m,b_m]$ and $[a_n,b_n]$ gives \begin{align*} |p_m-p_n| \leq (b_m-a_m)/2+(b_n-a_n)/2. \end{align*} The chosen intervals satisfy $b_i-a_i \leq 2^{-(i+2)}$ for each index $i$, so \begin{align*} |p_m-p_n| \leq 2^{-(m+3)}+2^{-(n+3)}. \end{align*} Since $2^{-(i+3)} \leq 2^{-i}$ for every $i \in \mathbb{N}$, this implies \begin{align*} |p_m-p_n| \leq 2^{-m}+2^{-n}. \end{align*} This is exactly the regular Cauchy condition required in the theorem statement. [/guided] [/step] [step:Build a located cut from a regular Cauchy sequence] Let $q: \mathbb{N} \to \mathbb{Q}$ be a regular Cauchy sequence. Define $L_q \subset \mathbb{Q}$ by $r \in L_q$ if and only if there exists $n \in \mathbb{N}$ such that $r+2^{-n}<q_n$. The set $L_q$ is downward closed because if $s \leq r$ and $r+2^{-n}<q_n$, then $s+2^{-n} \leq r+2^{-n}<q_n$. It is rounded because if $r+2^{-n}<q_n$, choose a rational $t$ with $r<t<q_n-2^{-n}$; then $r<t$ and $t \in L_q$. It is inhabited because $q_1-1 \in L_q$, after replacing the harmless constant $1$ by any rational larger than $2^{-1}$. It is proper because regularity gives $q_n \leq q_1+2^{-n}+2^{-1}$ for every $n$, so any rational $u>q_1+2$ cannot satisfy $u+2^{-n}<q_n$. It remains to check locatedness. Let $r<s$ in $\mathbb{Q}$. Choose $k \in \mathbb{N}$ such that $2^{2-k}<s-r$, which is possible by the [Archimedean property](/theorems/737) of $\mathbb{Q}$. Since order on $\mathbb{Q}$ is decidable, either $r+2^{-k}<q_k$ or $q_k \leq r+2^{-k}$. In the first case, $r \in L_q$. In the second case, for every $j \in \mathbb{N}$ the regularity estimate gives $q_j \leq q_k+2^{-j}+2^{-k}$, hence $q_j-2^{-j} \leq q_k+2^{-k} \leq r+2^{1-k}<s$. Thus $s+2^{-j}<q_j$ is impossible for every $j$, so $s \notin L_q$. Therefore $L_q$ is located. [/step] [step:Recover a cut from its chosen Cauchy approximation] Let $L$ be a located Dedekind cut, let $((a_n,b_n))_{n \in \mathbb{N}}$ be the chosen admissible intervals, and let $p_n=(a_n+b_n)/2$. We prove that $L_p=L$. First suppose $r \in L$. By roundedness, choose $t \in \mathbb{Q}$ with $r<t$ and $t \in L$. Choose $n$ so large that $2^{-n}+2^{-(n+3)}<t-r$. Since $t \in L$ and $b_n \notin L$, we must have $t \leq b_n$; otherwise $b_n<t$ and downward closure would give $b_n \in L$. Hence $p_n \geq b_n-(b_n-a_n)/2 \geq t-2^{-(n+3)}$. Therefore \begin{align*} r+2^{-n}<t-2^{-(n+3)} \leq p_n. \end{align*} Thus $r \in L_p$. Conversely suppose $r \in L_p$. Then for some $n \in \mathbb{N}$, $r+2^{-n}<p_n$. Since $b_n-a_n \leq 2^{-(n+2)}$, we have $p_n \leq a_n+2^{-(n+3)}$. Therefore \begin{align*} r<a_n+2^{-(n+3)}-2^{-n}<a_n. \end{align*} Because $a_n \in L$ and $L$ is downward closed, $r \in L$. Hence $L_p=L$. [/step] [step:Recover a regular Cauchy sequence up to Cauchy equality] Let $q: \mathbb{N} \to \mathbb{Q}$ be a regular Cauchy sequence and form the cut $L_q$. Choose admissible intervals $(a_n,b_n)$ for $L_q$ and put $p_n=(a_n+b_n)/2$. We prove $p \sim q$. Fix $n \in \mathbb{N}$. Since $a_n \in L_q$, there is $j \in \mathbb{N}$ such that $a_n+2^{-j}<q_j$. Regularity gives $q_j \leq q_n+2^{-j}+2^{-n}$, hence $a_n<q_n+2^{-n}$. Since $b_n \notin L_q$, the defining condition for $L_q$ fails at index $n$, so $b_n+2^{-n}<q_n$ is false; equivalently, $q_n \leq b_n+2^{-n}$. Combining these inequalities with $a_n \leq p_n \leq b_n$ and $b_n-a_n \leq 2^{-(n+2)}$ gives \begin{align*} q_n-p_n \leq b_n+2^{-n}-a_n \leq 2^{-n}+2^{-(n+2)}. \end{align*} Similarly, \begin{align*} p_n-q_n \leq b_n-a_n+2^{-n} \leq 2^{-n}+2^{-(n+2)}. \end{align*} Thus $|p_n-q_n| \leq 2^{-n}+2^{-(n+2)}$ for every $n$. Given any $\varepsilon \in \mathbb{Q}_{>0}$, choose $N$ such that $2^{-N}+2^{-(N+2)}<\varepsilon$. For every $n \geq N$, monotonicity of powers of $2$ gives $|p_n-q_n|<\varepsilon$. Therefore $p \sim q$. [/step] [step:Conclude the comparison is inverse on the stated quotient objects] The previous two steps prove the two inverse statements required by the theorem. Starting from a located Dedekind cut $L$, choosing admissible rational intervals, and passing through the Cauchy lower-cut construction gives the same cut $L$. Starting from a regular Cauchy sequence $q$, passing to $L_q$, choosing admissible rational intervals, and taking midpoints gives a regular Cauchy sequence Cauchy-equal to $q$. Therefore the Cauchy-to-Dedekind and Dedekind-to-Cauchy constructions are mutually inverse after quotienting regular Cauchy sequences by $\sim$ and identifying Dedekind reals by equality of cuts. [/step]