I'm doing some archeology and trying to understand a claim. As summed up by David Roberts, on the FOM list in 2011:
Let the statement "every infinite sequence of rationals in [0,1] has an infinite Cauchy 1/n subsequence" be denoted CSR. I have seen [Friedman] make this similar statements involving CSR several times…
In this MO answer, Andrej Bauer notes that CSR is false in the effective topos:
Consider a Specker sequence which has no accumulation point in a strong sense, so it cannot have a convergent subsequence.
What I'm currently puzzling over is that CSR appears false classically, too. Let $F$ be the Fibonacci sequence, and let $p$ be the sequence of Padé approximants to the golden ratio $\phi$, or rather to the conjugate golden ratio $\phi - 1$:
$$p_i = \frac{F_i}{F_{i+1}}$$
$p$ satisfies CSR; it converges to $\phi - 1$. But now define the sequence $q$:
$$q_i = \sum_{0}^{i}{p_i} \pmod{1}$$
$q$ is quasirandom and should visit every Cauchy bucket infinitely often, just like $\phi$. I wrote some Python code to verify this claim; try something like asBuckets(f, 400, 8) to take $q_{400}$ with $2^8$ binary Cauchy buckets. At the same time, $q : \mathbb{N} \to \mathbb{Q}$ is an infinite sequence of rationals.
I think that Friedman knew all of this. So, what hidden assumptions are not stated in Friedman's wording of CSR?
