[proofplan] Apply the completion operation to the given sequence and its modulus. The operation returns the point $x=\lim_N x_n$. Its compatibility property is exactly the desired quantitative estimate, so the proof is an unpacking of the displayed completion data rather than an additional compactness or choice argument. [/proofplan] [step:Apply the completion operation] Let $(x_n)_{n\in\mathbb{N}}$ be a sequence in $X$ with modulus of Cauchy convergence $N$. By the assumed Cauchy-completion operation, the pair consisting of the sequence and the modulus determines a point \begin{align*} x=\lim_N x_n \end{align*} in $X$. [guided] The input data are the sequence $(x_n)_{n\in\mathbb{N}}$ and the modulus $N:\mathbb{N}\to\mathbb{N}$ satisfying the Cauchy tail estimate. The completion operation is defined on exactly this kind of input, so it returns the point $x=\lim_N x_n$ in $X$. [/guided] [/step] [step:Use the compatibility estimate] Fix $k\in\mathbb{N}$ and $n\geq N(k+1)$. The compatibility property of the completion operation, applied to the same sequence and the same modulus $N$, gives \begin{align*} d(x_n,\lim_N x_n)\leq 2^{-k}. \end{align*} Since $x=\lim_N x_n$, this is \begin{align*} d(x_n,x)\leq 2^{-k}. \end{align*} [guided] Take arbitrary $k\in\mathbb{N}$ and $n\geq N(k+1)$. The completion operation's compatibility property says directly that $d(x_n,\lim_N x_n)\leq 2^{-k}$. The point chosen in the previous step is $x=\lim_N x_n$, so the same inequality becomes $d(x_n,x)\leq 2^{-k}$. [/guided] [/step] [step:Conclude the quantitative Cauchy criterion] The point $x\in X$ constructed from the completion operation satisfies the required estimate for every $k\in\mathbb{N}$ and every $n\geq N(k+1)$. Therefore the sequence determines a [limit point](/page/Limit%20Point) with the advertised quantitative convergence bound. [/step]