Negative reciprocal: uniform one-step recursion of the Euclidean descent

Proved

burau_cf_std_neg_inv_step

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

continued-fractionseuclidean-algorithmreciprocity

Negative reciprocal of a rational: the uniform step of the Euclidean descent. For positive integers $a,b$ , the standard Euclidean continued fraction of $-1/(b/a) = -a/b$ takes the explicit one-step recursion

\mathtt{cfStd}(b,\,-a) = -\left\lceil \frac{a}{b}\right\rceil :: \mathtt{cfStd}\Bigl(b\left\lceil \frac{a}{b}\right\rceil - a,\ b\Bigr),

with no case distinction on the size of $a$ and $b$ : the leading quotient is the ceiling quotient of the negated dividend and the new pair is again positive. This is the recursion that drives the whole continued-fraction analysis of the transformation $x\mapsto -1/x$ , which is the missing input of the three-strand Burau faithfulness reduction.

Preamble

import Definitions.Def_burau_std_cf
import Theorems.Thm_burau_cf_ediv_neg_of_pos
import Theorems.Thm_burau_cf_emod_neg_of_pos

set_option autoImplicit false

Formal statement

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

Source

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

View graph