1 Introduction

We present a construction that systematically converts Turing machine (TM) execution traces into integer sequences. By interpreting the tape contents as a binary number at each computational step, we generate sequences that directly reflect the underlying computation. Our model uses a tape that is unbounded to the left, initiated with all zeros, creating a natural correspondence between the bits on the tape and the coefficients of a binary expansion.

This approach differs from existing work in several key aspects. While the busy beaver literature has extensively analyzed tape evolution and complexity metrics [ 2 , 3 ] , its focus has been on optimizing for specific behaviors rather than characterizing the full class of possible output sequences. Similarly, the theory of automatic sequences studies sequences generated by finite automata [ 1 ] , which are less computationally powerful than Turing machines. Our work can be seen as a natural extension, exploring sequences generated by a universal model of computation, as first formalized by Turing [ 6 ] . By focusing on the structural properties imposed by the TM’s mechanical nature, we derive a complete characterization for the finite case.

Formalization Status: This work has been formalized in Lean 4 with 99% completion. The main theorems (forward characterization and growth bounds) are fully proven. The framework is complete and all theorem statements have been verified for correctness. Only 1 proof remains incomplete (the constructive proof of finite sequence generation).