Pure binary-size facts

Moved from the legacy binary calculus. No computability predicate is imported or introduced here. length_encNat_add_le keeps its legacy qualified name in ComputableTidilyInO, a staged cleanup item.

theorem Turing.MultiTapeTM.length_encNat_mono {m n : ℕ} (h : m ≤ n) : (encNat m).length ≤ (encNat n).length

The length of encNat is monotone.

theorem Turing.MultiTapeTM.two_pow_size_le_two_mul {n : ℕ} (hn : 0 < n) : 2 ^ n.size ≤ 2 * n

For positive n, the next power of two 2 ^ n.size is at most 2 * n.

theorem Turing.MultiTapeTM.ComputableTidilyInO.length_encNat_add_le (n i : ℕ) : (encNat (n + i)).length ≤ (encNat n).length + i

Adding i adds at most i bits.