Native binary-width measurement

The binary size of a runtime natural is computed by measuring its encoded digits. natSize returns that width in binary; natSizeUnary returns it in unary. Neither operation expands the original natural to unary.

theorem Turing.MultiTapeTM.ComputableInSpace.natSize : ComputableInSpace Nat.size encNat encNat fun (n : ℕ) => (encNat n).length

Measure the binary width of a runtime natural in linear encoded-input space.

theorem Turing.MultiTapeTM.ComputableInSpace.natSizeUnary : ComputableInSpace Nat.size encNat encUnary fun (n : ℕ) => (encNat n).length

The binary width, returned in unary, in linear encoded-input space.