Several of the most celebrated theorems in AIT, such as Symmetry of Information, employ programs that need to interpret other programs. So constants in these theorems significantly suffer from complicated index encodings.

A binary encoding is not as simple as you might think, as the code needs to be self-delimiting. So you first need to encode the number of bits used in the binary code. And that must also be self-delimiting. As you can see, you need to fall back to a unary encoding at some point, as that is naturally self-delimiting.

An example of an efficient binary self-delimiting code can be found at [1]. Note that the program for decoding it into a Church numeral (the very best case) is already about 60% the size of the entire self-interpreter.

Many programs used in AIT proofs use only single digit indices (the self-interpreter e.g. only uses 1-5) and these would be negatively impacted by a binary encoding.

[1] https://gist.github.com/tromp/86b3184f852f65bfb814e3ab0987d8...