Width-driven binary shift-and-add multiplication -- pure proofs

This file proves the generalized arithmetic invariant of the little-endian shift-and-add fold, its multiplication specialization, and width bounds for every partial accumulator and shifted multiplicand.

theorem Complexity.BinaryShiftMul.fold_eq_internal (bits : List Bool) (acc shift : ℕ) : fold bits acc shift = (acc + shift * Nat.fromBitsLE bits, shift * 2 ^ bits.length)

The generalized shift-and-add fold accumulates shift times the decoded bit string and doubles shift once per consumed bit.

theorem Complexity.BinaryShiftMul.fromBitsLE_take_le_internal (bits : List Bool) (i : ℕ) : Nat.fromBitsLE (List.take i bits) ≤ Nat.fromBitsLE bits

Taking a low-order prefix cannot increase its little-endian decoded value.

theorem Complexity.BinaryShiftMul.fold_take_eq_internal (lhs rhs i : ℕ) (hi : i ≤ rhs.size) : fold (List.take i rhs.bits) 0 lhs = (partialAcc lhs rhs i, partialShift lhs i)

If the iteration index is within the canonical multiplier width, folding its prefix produces the advertised partial accumulator and shift.

theorem Complexity.BinaryShiftMul.step_partial_internal (lhs rhs i : ℕ) (hi : i < rhs.size) : step (rhs.bits.get ⟨i, ⋯⟩) (partialAcc lhs rhs i) (partialShift lhs i) = (partialAcc lhs rhs (i + 1), partialShift lhs (i + 1))

One live multiplier bit advances the partial arithmetic invariant by one iteration.

theorem Complexity.BinaryShiftMul.fold_natBits_internal (lhs rhs : ℕ) : fold rhs.bits 0 lhs = (lhs * rhs, lhs * 2 ^ rhs.size)

Folding all canonical multiplier bits computes multiplication and leaves the shift advanced by the multiplier width.

theorem Complexity.BinaryShiftMul.partialAcc_full_internal (lhs rhs : ℕ) : partialAcc lhs rhs rhs.size = lhs * rhs

The complete partial accumulator is the product.

theorem Complexity.BinaryShiftMul.partialShift_full_internal (lhs rhs : ℕ) : partialShift lhs rhs.size = lhs * 2 ^ rhs.size

The complete partial shift has advanced by the multiplier width.

theorem Complexity.BinaryShiftMul.fold_natBits_fst_internal (lhs rhs : ℕ) : (fold rhs.bits 0 lhs).1 = lhs * rhs

The accumulator component of the complete pure fold is the product.

theorem Complexity.BinaryShiftMul.partialAcc_le_mul_internal (lhs rhs i : ℕ) : partialAcc lhs rhs i ≤ lhs * rhs

Every partial accumulator is bounded by the complete product.

theorem Complexity.BinaryShiftMul.size_mul_le_add_internal (lhs rhs : ℕ) : (lhs * rhs).size ≤ lhs.size + rhs.size

Binary width is subadditive under multiplication.

theorem Complexity.BinaryShiftMul.partialAcc_size_le_width_internal (lhs rhs i : ℕ) : (partialAcc lhs rhs i).size ≤ lhs.size + rhs.size

Every partial accumulator fits in the combined input width.

theorem Complexity.BinaryShiftMul.partialShift_size_le_internal (lhs i : ℕ) : (partialShift lhs i).size ≤ lhs.size + i

Shifting left by i grows binary width by at most i.

theorem Complexity.BinaryShiftMul.partial_widths_le_internal (lhs rhs i : ℕ) (hi : i ≤ rhs.size) : (partialAcc lhs rhs i).size ≤ lhs.size + rhs.size ∧ (partialShift lhs i).size ≤ lhs.size + rhs.size

At any live multiplier iteration, both arithmetic values fit in the combined input width.