If the number representation is encoded outside the 64 bits then you have removed the 64 bit restriction. Of course it is hard to calculate how many bits of information are required to define the type. But "uint64" is pretty small and just requires our current human context (quite a few more bits of information) to make sense!
> If the number representation is encoded outside the 64 bits then you have removed the 64 bit restriction.
The explanation for how to interpret the 64 bit string is always outside of the 64 bit string. It's going to be tough to compare how big two explanations are since that's going to depend a lot on what each person considers to be a sufficient explanation.
I'm personally quite rusty on lambda calculus, and from glancing at the author's papers about lambda calculus encodings I suspect it will take a rather large number of bytes to represent an explanation that will make it through my thick skull!
