Binary word arithmetic and comparison

The carry fold, its value and length laws, and the highest-differing-bit characterization of strict order are pure facts about least-significant-first binary words. They do not import a computability calculus. The multiplication bit fold and its prefix-size laws are shared with the direct and legacy resource proofs, retaining the original shift-and-add data.

theorem Turing.MultiTapeTM.NatAdd.bits_bit (b : Bool) (n : ℕ) (h : n = 0 → b = true) : (2 * n + b.toNat).bits = b :: n.bits

The binary digits of 2 * n + b, if they do not end in a zero.

def Turing.MultiTapeTM.NatAdd.carry (a b c : Bool) : Bool

The carry of adding three digits.

def Turing.MultiTapeTM.NatAdd.addBits : Bool → List Bool → List Bool → List Bool

Adds the digits l and r with the carry c, least significant first; r is padded with zeros.

theorem Turing.MultiTapeTM.NatAdd.incr_bits (c : Bool) (n : ℕ) : NatSucc.incr c n.bits = (n + c.toNat).bits

Incrementing a canonical word represents addition of its incoming carry.

theorem Turing.MultiTapeTM.NatAdd.addBits_bits (c : Bool) (m n : ℕ) : addBits c m.bits n.bits = (m + n + c.toNat).bits

The word adder computes the sum of two natural numbers and an incoming carry.

def Turing.MultiTapeTM.NatAdd.addStep (s : Bool × List Bool × List Bool) (a : Bool) : Bool × List Bool × List Bool

One round: add the digit a, the next digit of the rest r and the carry c.

theorem Turing.MultiTapeTM.NatAdd.foldl_addStep (l : List Bool) (c : Bool) (r out : List Bool) : have s := List.foldl addStep (c, r, out) l; out ++ addBits c l r = s.2.2 ++ NatSucc.incr s.1 s.2.1

The fold invariant splits the accumulated digits from the remaining carry addition.

theorem Turing.MultiTapeTM.NatAdd.length_foldl_addStep (l : List Bool) (s : Bool × List Bool × List Bool) : (List.foldl addStep s l).2.1.length ≤ s.2.1.length ∧ (List.foldl addStep s l).2.2.length = s.2.2.length + l.length

Each round consumes at most one remaining digit and emits exactly one output digit.

Binary multiplication fold

The existing NatMul word-fold data and laws are moved from Complexity/Arith with Christian Reitwiessner's source and proof bodies unchanged. Only these four previously module-private names are exposed for shared direct and legacy resource proofs.

def Turing.MultiTapeTM.NatMul.mulStep (s : ℕ × ℕ) (a : Bool) : ℕ × ℕ

One round: add the shifted factor s.2 to the product s.1 if the digit a is 1, and shift the factor.

theorem Turing.MultiTapeTM.NatMul.foldl_mulStep (m acc sh : ℕ) : (List.foldl mulStep (acc, sh) m.bits).1 = acc + m * sh

The bit fold multiplies the shifted factor and adds the initial accumulator.

theorem Turing.MultiTapeTM.NatMul.foldl_mulStep_le (l : List Bool) (acc sh : ℕ) : (List.foldl mulStep (acc, sh) l).1 + sh ≤ acc + 2 ^ l.length * sh ∧ (List.foldl mulStep (acc, sh) l).2 = 2 ^ l.length * sh

Prefix accumulators and shifts are bounded by the number of processed binary digits.

theorem Turing.MultiTapeTM.NatMul.size_le_of_le {x n : ℕ} (i : ℕ) (h : x ≤ 2 ^ i * n) : x.size ≤ i + n.size

A shifted numerical bound gives an additive bound on binary size.

theorem Nat.lt_iff_exists_testBit (m n : ℕ) : m < n ↔ ∃ i < n.size, m.testBit i = false ∧ n.testBit i = true ∧ ∀ j < m.size + n.size, i < j → m.testBit j = n.testBit j

m < n exactly when some bit position below the length of n holds a zero in m and a one in n, and every higher position below the total length agrees.