The source reduces to the snake lemma in its general form ($Transducers.boundedWidth_isRegular$, $PartC/SnakeReg.lean$): a halting run visits every column at most $|Q|$ times, so the function is its own width-$|Q|$ output function, and the width-$k$ output function is regular by induction on $k$, cutting the run at the record-breaking columns into looping and progressing parts of smaller width ($PartC/SnakeWalk.lean$, $PartC/SnakeRec.lean$, $PartC/SnakeLoop.lean$, the $PartC/SnakeChk*.lean$ family) and gluing them with Lemma C.2.10.

Theorem C.2.9 of Transducers, Part C; formalised by Aristotle (Harmonic).