[codeismightier]

Intriguing claim! At first I was skeptical, thinking that there would be an issue with leading zeros being discarded. However, with some piloting, I was able to use Claude and ChatGPT to construct a proof of your claim.

Sketch of the argument:

First, an arithmetic coder maps strings to non-overlapping subintervals of [0, 1) that respect lexicographic order.

Second, the process of emitting the final encoding preserves this. If enc(s) ∈ I(s), enc(t) ∈ I(t), and I(s) <= I(t), then enc(s) <= enc(t).

Finally, binary fractions compared left-to-right bitwise yield the same order as their numerical values — this is just memcmp.

Thus, we have a proof of your claim that arithmetic coding preserves lexicographic order! Nice result!

My mistake was in thinking that leading zeros are discarded -- it is tailing zeros that are discarded!