The descent section equals terminal value times recorded word
Provedburau_rho_eq_baseQ_cfWordbraid-groupscontinued-fractionsdescent-sectionsl2z
The descent section is the terminal value times the recorded word. For every integer matrix ,
where is the quotient list of the Euclidean descent, is the terminal matrix it reaches, is the explicit terminal value, and turns the quotient list into the product of the descent factors in the reduced braid quotient . The proof is a strong induction on the descent measure . Together with the -rule this is the structural description of that turns the two multiplication rules into a proof of for words in the braid group, and hence into the reduction of the milestone frontier to the continued-fraction -rule.
Preamble
import Definitions.Def_burau_cf_list import Definitions.Def_burau_rho import Definitions.Def_burau_reduced_braid_group set_option autoImplicit false
Formal statement
theorem burau_rho_eq_baseQ_cfWord (M : BurauNC.M2) :
BurauNC.rho M = BurauNC.baseQ (BurauNC.cfEnd M) * BurauNC.cfWord (BurauNC.cfList M) :=
by sorry
Source
Euclidean algorithm in SL(2,Z) and the reduced Burau representation; cf. C. Moser, H. S. M. Coxeter, *Generators and relations for discrete groups* (1964), Ch. 3.