Pure binary-size facts

Moved unchanged from the legacy binary calculus, retaining its existing qualified names. No computability predicate is imported or introduced here; the names remain a staged cleanup item.

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

The length of encNat is monotone.

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.