Continued fractions recover $j/\gcd(j,r)$ and $r/\gcd(j,r)$ from an approximation within $1/(2r^2)$

Let $j \ge 0$ and $r \ge 1$ be integers and let $\varphi$ be a real number with

Then some convergent of the continued fraction expansion of $\varphi$ equals

in lowest terms; that is, the continued fractions algorithm run on $\varphi$ recovers both $j/\gcd(j,r)$ and $r/\gcd(j,r)$.

This is the classical post-processing step that turns the measured approximation of a phase $j/r$ into the reduced fraction itself.

Formalization Note The article states the hypothesis with $\le$; it is formalized with strict $<$. With $\le$ the statement fails for the standard continued fraction expansion used by Mathlib's Real.convergent: for $j = r = 1$ and $\varphi = 1/2$ one has $|1 - 1/2| = 1/(2\cdot 1^2)$, but the convergents of $1/2$ are $0$ and $1/2$, never $1$. In the application the inequality is strict (milestone register size bound and $r < N$). The article's hypothesis "$j$ and $r$ are $n$-bit integers" places no restriction and is omitted.