Linear binary addition -- resource-bound internals

This file relates the concrete scan and composed-machine bounds to the standard binary widths of the two operands.

theorem Complexity.TM.size_add_le_max_add_one_internal (lhs rhs : ℕ) : (lhs + rhs).size ≤ max lhs.size rhs.size + 1

theorem Complexity.TM.binaryRippleAddTime_le_internal (lhs rhs : ℕ) : binaryRippleAddTime lhs rhs ≤ 3 * (lhs.size + rhs.size) + 14