Shift lemma for the standard Euclidean continued fraction

Proved

burau_cf_std_add_divisor

by lt9 · Sep 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

continued-fractionseuclidean-algorithmtermination

Shift lemma for the standard Euclidean continued fraction. For $r\neq 0$ ,

\mathtt{cfStd}(r,\ r+a) = \left(\frac{a}{r}+1\right) :: \mathtt{cfStd}\bigl(a\bmod r,\ r\bigr),

i.e. adding the divisor $r$ to the dividend increases the first quotient by one and leaves the remainder, hence the whole tail, unchanged. This is exactly the step at which the two Euclidean descents appearing in the continued-fraction analysis merge, and it is what makes the assembled two-branch formula for the negative reciprocal of a rational a theorem rather than a numerical observation.

Preamble

import Definitions.Def_burau_std_cf

set_option autoImplicit false

Formal statement

theorem burau_cf_std_add_divisor (r a : ℤ) (hr : r ≠ 0) :
    cfStd r (r + a) = (a / r + 1) :: cfStd (a % r) r := by sorry

Source

Euclidean continued fractions; cf. A. Ya. Khinchin, *Continued Fractions* (1964), Ch. II.

View graph