Part 2 of 2

TheoremStrict growth of continued-fraction denominators#✓fully proved

Let \(K\) be a linearly ordered field with a floor function, let \(v \in K\), and write \(v = [a_0; a_1, a_2, \dots]\) for its regular continued fraction, with convergent denominators \(q_0 = 1\), \(q_1 = a_1\) and \(q_{k+2} = a_{k+2} q_{k+1} + q_k\). For every natural number \(n\), if the partial quotient \(a_{n+2}\) exists (the continued fraction has not terminated before it), then \(q_{n+1} < q_{n+2}\).

The comparison starts at \(q_1\) because \(q_0 = 1\) while \(q_1 = a_1\) can also equal \(1\).

theorem of_den_succ_lt_succ_succ (n : ℕ)
    (not_terminatedAt : ¬(GenContFract.of v).TerminatedAt (n + 1)) :
    (GenContFract.of v).dens (n + 1) <
      (GenContFract.of v).dens (n + 2)

Sources

• arXiv:2607.23662, item D07, which uses the adjacent inequality \(q_{k-1} < q_k\).

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.