Euclidean division of a negated dividend (ceiling form)

Proved

burau_cf_ediv_neg_of_pos

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

arithmeticcontinued-fractionseuclidean-algorithm

Euclidean division of a negated dividend. For positive integers $a,b$ , the Euclidean quotient of $-a$ by $b$ is minus the ceiling of $a/b$ :

\frac{-a}{b} = -\left\lceil \frac{a}{b}\right\rceil = -\frac{a+b-1}{b},

where the last quotient is the integer division. This uniform formula (no case distinction on the size of $a$ and $b$ ) is the arithmetic input that makes the continued-fraction rule $x\mapsto -1/x$ a single recursion instead of a case analysis; it is used in the Euclidean-descent analysis of $\mathrm{SL}(2,\mathbb Z)$ behind the three-strand Burau faithfulness statement.

Preamble

import Mathlib

set_option autoImplicit false

Formal statement

theorem burau_cf_ediv_neg_of_pos (a b : ℤ) (ha : 0 < a) (hb : 0 < b) :
    (-a) / b = -((a + b - 1) / b) := by sorry

Source

Euclidean algorithm on Z; cf. A. Ya. Khinchin, *Continued Fractions* (1964), Ch. II.

View graph