Linear-time canonical binary addition -- pure proofs

This file proves that the finite full-adder recurrence computes addition on canonical little-endian Nat.bits. The generalized theorem includes an incoming carry so that its induction follows the recurrence exactly.

theorem Complexity.BinaryRippleAdd.ripple_natBits_carry_internal (carry : Bool) (lhs rhs : ℕ) : ripple carry lhs.bits rhs.bits = (lhs + rhs + if carry = true then 1 else 0).bits

Ripple addition with an incoming carry computes the corresponding natural sum. This is the induction-strengthened form of ripple_natBits_internal.

theorem Complexity.BinaryRippleAdd.ripple_natBits_internal (lhs rhs : ℕ) : ripple false lhs.bits rhs.bits = (lhs + rhs).bits

Ripple addition without an incoming carry computes canonical addition.

theorem Complexity.BinaryRippleAdd.length_ripple_natBits_internal (lhs rhs : ℕ) : (ripple false lhs.bits rhs.bits).length = (lhs + rhs).size

The pure result has exactly the canonical width of the sum.

theorem Complexity.TM.binaryRippleAddScanTime_natBits_internal (lhs rhs : ℕ) : binaryRippleAddScanTime lhs.bits rhs.bits = max lhs.size rhs.size + 1

Rewrite the list-level scan bound as a bound in natural-number widths.