Is it possible to get rid of the small correction terms such as in Theorem 5.3? Note that the construction in the proof shows that KE(x) is actually bounded by KE(s), the complexity of the enumerable number with minimal KT(s). The facts , , , as well as intuition and wishful thinking inspired by Shannon-Fano Theorem [#!Shannon:48!#] and Coding Theorem 5.1 suggest there might indeed be tighter bounds: