USize.size_eq

theorem USize.size_eq : USize.size = 2 ^ System.Platform.numBits

This theorem states that the size of an unsigned machine integer (`USize.size`) is equal to `2` raised to the power of the number of bits in the platform architecture (`System.Platform.numBits`). In other words, the number of distinct values that an unsigned machine integer can represent is exactly the total number of different bit patterns that can be represented with the word size of the platform, which is either 32 or 64 bits.

More concisely: The size of an unsigned machine integer (`USize`) is equal to 2 raised to the number of bits in the platform architecture (`System.Platform.numBits`). Equivalently, the number of distinct values an unsigned machine integer can represent is 2 raised to the word size of the platform.