The Exercise

Let $\varphi$ be a real number and $s/r$ a rational number in lowest terms, with $r \ge 1$. The theorem says that if $|\varphi - s/r| \le 1/(2r^2)$, then $s/r$ is one of the rational numbers obtained by truncating, at some step, the expansion of $\varphi$ into integer parts described below. The bound $1/(2r^2)$ is the one in Legendre’s theorem.

Continued Fractions

The continued fraction of a real number $\varphi$ is the sequence of integers $a_0, a_1, a_2, \dots$ obtained by taking integer parts and inverting remainders: starting from $\varphi_0 = \varphi$, $$a_k = \lfloor \varphi_k \rfloor, \qquad \varphi_{k+1} = \frac{1}{\varphi_k - a_k},$$(1) and the sequence ends at $a_k$ when $\varphi_k$ is an integer.

The $n$th convergent of $\varphi$ is the rational number obtained by stopping the expansion at $a_n$, $$[a_0; a_1, \dots, a_n] = a_0 + \dfrac{1}{a_1 + \dfrac{1}{\;\ddots\; + \dfrac{1}{a_n}}}.$$(2)

The Claim

This is the negation of the book’s theorem, with its bound exactly as the book writes it.

What Is Checked

The claim is stated over the real numbers, the rational numbers with their denominators in lowest terms, and the continued fraction (1) of a real number with its convergents (2). What the library proves about these constructions is the existence of the counterexample (3).