Is this a theorem or a conjecture?

A few months ago, I read The Irrationals by Julian Havil. I remember reading that if you order the rationals between 0 and 1 in this way: $\frac{1}{2},\frac{1}{3},\frac{2}{3},\frac{1}{4},\frac{2}{4},\frac{3}{4},\frac{1}{5},\cdots$ and then construct intervals, the first one being $[\frac{1}{3},\frac{1}{2}]$ and the following ones being constructed from the next two (not necessarily consecutive) terms in the sequence that are included in the last constructed interval, you get smaller and smaller intervals converging to a single point: $\sqrt2 - 1$.

My question is whether this result was arrived at numerically or is there a formal proof? [and if the latter, what is the proof or where can I find it?] The wording in the book did not make this very clear, if I recall correctly.

First few intervals : $(1/3,1/2),(2/5,3/7),(7/17,5/12),(12/29,17/41),...$

The general construction is related to the Farey sequence.

Define freshman's sum $\frac{a}{b}\oplus \frac{c}{d}=\frac{a+c}{b+d}$.

This sum satisfies the median property : $\frac{a}{b}<\frac{c}{d}\Rightarrow \frac{a}{b}<\frac{a}{b}\oplus \frac{c}{d}<\frac{c}{d}$.

Then, the intervals are constructed as the following rule :

Start with $\frac{1}{3}<\frac{1}{2}$. Then add the (freshman's sum) $\frac{1}{3}\oplus \frac{1}{2}=\frac{2}{5}$, which is the next entry of the sequence between $\frac{1}{2}$ and $\frac{1}{3}$.

Now the modified sequence of appearing fractions is $\frac{1}{3}<\frac{2}{5}<\frac{1}{2}$. As we know, the next entry appearing is $\frac{2}{5}\oplus\frac{1}{2}=\frac{3}{7}$.(the sum of leftmost two has greater denominator than this sum, so this sum should appear first.)

So the modified sequence in this step is $\frac{1}{3}<\frac{2}{5}<\frac{3}{7}<\frac{1}{2}$.

Note that the second interval $(\frac{2}{5},\frac{3}{7})$ is constructed from this sequence in this step.

In the next step, the fraction added is $\frac{2}{5}\oplus\frac{3}{7}=\frac{5}{12}$(Note that we should find a number between the second interval $(\frac{2}{5},\frac{3}{7})$), and the modified seq is $\frac{1}{3}<\frac{2}{5}<\frac{5}{12}<\frac{3}{7}<\frac{1}{2}$.

Following step add $\frac{2}{5}\oplus\frac{5}{12}=\frac{7}{17}$(sum with less-denominator one) to the modified seq and we get the third interval $(\frac{7}{17},\frac{5}{12})$.

Now I think you'll be able to develop all following step with ease; in summary, choosing the terms in the sequence corresponds to the freshman's sum in Farey sequence, and the intervals constructed is the center two terms in the modified sequence in each even step.

Because the intervals are determined in each even step, I'll describe the patterns of the modified sequence in even steps from now on.

As you can check, the order relation between the center two terms reverses as 2 steps go along, thus our algorithm is a period 4 calculation, i.e, starting with $\frac{1}{3}<\frac{1}{2}$, we proceed the following 4 sum in one period:

Start at the centermost two fractions, say $A,B$.

$\cdots < A<B<\cdots \Rightarrow \cdots < A < A\oplus B < B < \cdots$ $ \Rightarrow \cdots < A < A\oplus B <(A\oplus B)\oplus B < B < \cdots$ $\Rightarrow \cdots < A < A\oplus B <(A\oplus B )\oplus \left\{(A\oplus B)\oplus B\right\}<(A\oplus B)\oplus B < B < \cdots$ $\Rightarrow \cdots < A < A\oplus B<(A\oplus B)\oplus [(A\oplus B )\oplus \left\{(A\oplus B)\oplus B\right\}] <(A\oplus B )\oplus \left\{(A\oplus B)\oplus B\right\}<(A\oplus B)\oplus B < B < \cdots$

Then retake the centermost two terms in the final sequence and iterate the above algorithm.

Hence, the $(2n+1)$th interval is $\left( (A\oplus B)\oplus [(A\oplus B )\oplus \left\{(A\oplus B)\oplus B\right\}] ,(A\oplus B )\oplus \left\{(A\oplus B)\oplus B\right\}\right)$, where $(A,B)$ is the $(2n-1)$th interval.

Let the two endpoints of the $(2n-1)$th inverval $\frac{a_n}{c_n} < \frac{b_n}{d_n}$.

This sequence $a_n,b_n,c_n,d_n$ satisfies the following recurrence formula:

$a_{n+1}=3a_n+4b_n, b_{n+1}=2a_n+3b_n, c_{n+1}=3c_n+4d_n, d_{n+1}=2c_n+3d_n$

($a_1=b_1=1,c_1=3,d_1=2$)

$\therefore \begin{pmatrix} a_n&c_n \\ b_n & d_n \end{pmatrix}= \begin{pmatrix} 3&4 \\ 2& 3 \end{pmatrix}^{n-1}\begin{pmatrix} a_1 &c_1 \\ b_1 & d_1 \end{pmatrix}= \begin{pmatrix} 3&4 \\ 2& 3 \end{pmatrix}^{n-1}\begin{pmatrix} 1 &3 \\ 1 & 2 \end{pmatrix}$

$\therefore a_n=\frac{1+\sqrt{2}}{2}\xi_1^{n-1}-\frac{\sqrt{2}-1}{2}\xi_2^{n-1},b_n=\frac{2+\sqrt{2}}{4}\xi_1^{n-1}+\frac{2-\sqrt{2}}{4}\xi_2^{n-1},c_n=\frac{\xi_1^n+\xi_2^n}{2},d_n=\frac{4+3\sqrt{2}}{4}\xi_1^{n-1}+\frac{4-3\sqrt{2}}{4}\xi_2^{n-1}$

($\xi_1=3+2\sqrt{2},\xi_2=3-2\sqrt{2}$)

$\therefore \lim_{n\to \infty}\frac{a_n}{c_n}=\lim_{n\to \infty}\frac{b_n}{d_n}=\sqrt{2}-1$

P.S. The fractions in some interval $(a,b)$ indeed lies between $a$ and $b$ in a Farey sequence(at least one of order the denominator of this fraction).

And, if $\frac{p}{q}$ has neighbors $a,b$ in some Farey sequence, then $\frac{p}{q}=a\oplus b$.

Because we find the numbers first appearing in a squence having lexicographic order in each step, it is obviouse that if $\frac{p}{q}$ is the first-appearing fraction between $a$ and $b$, then $\frac{p}{q}$ has neighbors $a,b$ in $q$th Farey seqence.

To find properties I mentioned, this wikipedia page would be helpful.