Binary sizes of sums, products, powers, and factorials

Most of these pure facts are moved unchanged from the binary arithmetic facade. They retain their qualified names without depending on a machine calculus. The bounds Nat.size_add_le, Nat.size_add_le_max and Nat.size_le_self on the binary lengths of sums and of a number itself also serve the logarithmic terms of Kolmogorov complexity. Nat.size_eq_log_two_add_one, Nat.size_le_log_two_add_one and Nat.log2_eq_size_sub_one relate the binary length to ⌊log₂ n⌋, and Nat.log2_le_size compares the floor binary logarithm with the binary length.

theorem Nat.size_mul_le (m n : ℕ) : (m * n).size ≤ m.size + n.size

The binary length of a product is at most the binary lengths of the factors together.

theorem Nat.size_pow_le (m k : ℕ) : (m ^ k).size ≤ k * m.size + 1

The binary length of a power is at most the exponent times the binary length of the base, plus one for the zeroth power.

theorem Nat.size_factorial_le (n : ℕ) : n.factorial.size ≤ n * n.size + 1

The binary length of n! is at most n * n.size + 1.

theorem Nat.size_add_le (m n : ℕ) : (m + n).size ≤ m.size + n.size + 1

The binary length of a sum is at most the binary lengths of the summands together, plus one.

theorem Nat.size_add_le_max (m n : ℕ) : (m + n).size ≤ max m.size n.size + 1

The binary length of a sum is at most one more than the longer binary length of the summands.

theorem Nat.size_le_self (n : ℕ) : n.size ≤ n

A binary length is at most the number itself.

theorem Nat.size_eq_log_two_add_one {n : ℕ} (hn : n ≠ 0) : n.size = log 2 n + 1

The binary length of a positive number is ⌊log₂ n⌋ + 1.

theorem Nat.size_le_log_two_add_one (n : ℕ) : n.size ≤ log 2 n + 1

The binary length is at most ⌊log₂ n⌋ + 1, with equality unless n = 0.

theorem Nat.log2_eq_size_sub_one (n : ℕ) : n.log2 = n.size - 1

⌊log₂ n⌋ is one less than the binary length of n; both vanish at n = 0.

theorem Nat.log2_le_size (n : ℕ) : n.log2 ≤ n.size

The floor binary logarithm is at most the binary length.