Negative reciprocal of one: base case of the continued-fraction rule

Proved

burau_cf_std_neg_self

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

continued-fractionseuclidean-algorithmreciprocity

Base case of the negative-reciprocal rule of continued fractions. For $a\neq 0$ ,

\mathtt{cfStd}(a,\ -a) = [-1],

the continued fraction of $-1/1=-1$ . This is the base case of the inductive analysis of the transformation $x\mapsto-1/x$ : with the shift lemma and the two explicit branches for $b/a=1$ and $b/a\ge 2$ it anchors the computation of the quotient list of $-1/x$ from that of $x$ , which is the continued-fraction input of the three-strand Burau faithfulness reduction.

Preamble

import Definitions.Def_burau_std_cf

set_option autoImplicit false

Formal statement

theorem burau_cf_std_neg_self (a : ℤ) (ha : a ≠ 0) :
    cfStd a (-a) = [-1] := by sorry

Source

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

View graph