Arithmetic in binary within linear work space

The facts here bound lengths of arithmetic outputs and identify successor iteration, for clients with fixed workspace budgets. The certificate of binary addition, Turing.MultiTapeTM.ComputableInO.natAdd, is in Internal/BinaryAddition, which this file publicly imports: it is the linear zip-transducer certificate, weakened to time quadratic in the encoded input length and linear charged workspace.

Main results

• Turing.MultiTapeTM.length_encNat_add_le_add, .length_encNat_mul_le: lengths of sums and products in binary. Monotonicity, Turing.MultiTapeTM.length_encNat_mono, is in Internal/BinarySizeFacts.

theorem Turing.MultiTapeTM.length_encNat_eq_size (n : ℕ) : (encNat n).length = n.size

theorem Turing.MultiTapeTM.length_encNat_le_self (n : ℕ) : (encNat n).length ≤ n

A number is at least as large as its length.

theorem Turing.MultiTapeTM.length_encNat_add_le_add (a b : ℕ) : (encNat (a + b)).length ≤ (encNat a).length + (encNat b).length + 1

The binary length of a sum is bounded by the sum of the input lengths plus one.

theorem Turing.MultiTapeTM.length_encNat_mul_le (a b : ℕ) : (encNat (a * b)).length ≤ (encNat a).length + (encNat b).length

A product is at most as long as its factors together.

theorem Turing.MultiTapeTM.ComputableInO.iterate_succ_eq (k n : ℕ) : (fun (x : ℕ) => x + 1)^[k] n = n + k

theorem Turing.MultiTapeTM.ComputableTidilyInO.iterate_succ_eq (k n : ℕ) : (fun (x : ℕ) => x + 1)^[k] n = n + k