Negative reciprocal: first step of the Euclidean descent (remainder)

Proved

burau_cf_emod_neg_ge_one

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

continued-fractionseuclidean-algorithmreciprocity

First step of the negative-reciprocal rule of continued fractions (remainder form). For $a>0$ and $b/a\ge 1$ ,

(-a)\bmod b = b-a ,

the companion of $(-a)/b=-1$ . Together they show that the standard Euclidean descent applied to the pair $(b,-a)$ takes the explicit step $(b,-a)\mapsto(b-a,b)$ , the pivot of the analysis of the transformation $x\mapsto-1/x$ of continued fractions.

Preamble

import Mathlib

set_option autoImplicit false

Formal statement

theorem burau_cf_emod_neg_ge_one (a b : ℤ) (ha : 0 < a) (h : 1 ≤ b / a) :
    (-a) % b = b - a := by sorry

Source

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

View graph