The matrix quotient list equals the integer continued-fraction recursion

Proved

burau_cfList_eq_cfPair_v2

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

continued-fractionseuclidean-algorithmsl2z

The matrix descent and the integer descent compute the same quotient list. For every $2\times 2$ integer matrix $M$ ,

\mathtt{cfList}(M) = \mathtt{cfPair}\bigl(M_{00},\, M_{01}\bigr),

i.e. the quotient list recorded by the Euclidean descent step $M\mapsto (MT^{-n})S$ (with $n=M_{01}/M_{00}$ ) coincides with the purely integer recursion cfPair. The proof is a strong induction on the measure $|M_{00}|$ , using the measure lemma of the matrix descent. This bridges the matrix-level section of $\mathrm{SL}(2,\mathbb Z)$ and the integer continued-fraction machinery on which the negative-reciprocal rule is formalised.

Preamble

import Definitions.Def_burau_cf_list
import Definitions.Def_burau_cf_pair

set_option autoImplicit false

Formal statement

theorem burau_cfList_eq_cfPair_v2 (M : BurauNC.M2) :
    BurauNC.cfList M = BurauNC.cfPair (M 0 0) (M 0 1) := by sorry

Source

Euclidean algorithm in SL(2,Z); cf. C. Moser, H. S. M. Coxeter, *Generators and relations for discrete groups* (1964), Ch. 3.

View graph