The columns of a product, and the carry chain that adds one block of them

The schoolbook product of two P-bit numbers is a sum of columns, x · y = Σ_j c_j 2 ^ j, where c_j counts the pairs of set bits whose indices add to j – a count the Bit Sum Lemma delivers, one column at a time (DescriptiveComplexity.BitSum.mul_eq_colSum). What the Bit Sum Lemma does not deliver is the outer sum: summing the 2 P weighted columns is an iterated addition again, and every direct route to it fails – brute force, carries guessed for the whole product, digit tables, Chinese remainders.

The way out is the block split, taken once, plus a guessed carry chain per block. Cut the columns into blocks of g with 2 ^ g > P; the sum of one block is Σ_{t<g} c_{a+t} 2 ^ t, and adding it column by column keeps a running remainder below P – so the whole chain of a block is g remainders of g bits, which fits in one element and is laid out with the boundary-set device. That is exactly the “guess the carries” route that is ruled out for the whole product (there it is P remainders, one element cannot hold them); confined to a block it is affordable, and no further descent is needed.

This file is the ℕ side of that construction, with no structure in sight:

• DescriptiveComplexity.BitSum.intervalSum – the weighted sum of a range of columns, and its concatenation law (DescriptiveComplexity.BitSum.intervalSum_append);
• DescriptiveComplexity.BitSum.carryChain – the remainders of the column-wise addition, defined as quotients of the partial sums, with the three equations the certificate checks: the first column (DescriptiveComplexity.BitSum.carryChain_base), one step (DescriptiveComplexity.BitSum.carryChain_step), and the final remainder being the high bits (DescriptiveComplexity.BitSum.carryChain_last);
• DescriptiveComplexity.BitSum.eq_packVal_of_windows and DescriptiveComplexity.BitSum.packVal_evenOdd – reading a packed element off its windows, and re-assembling the even and the odd blocks into the sum of all columns;
• DescriptiveComplexity.BitSum.colWordN / DescriptiveComplexity.BitSum.colCountN – the word whose ones are one column, and the column count, with the product identity DescriptiveComplexity.BitSum.mul_eq_colSum.

Reading a bit as a number

theorem DescriptiveComplexity.BitSum.toNat_testBit (x i : ℕ) : (x.testBit i).toNat = x / 2 ^ i % 2

A bit, as the number it contributes: the digit of x at i.

theorem DescriptiveComplexity.BitSum.mod_two_pow_succ (x k : ℕ) : x % 2 ^ (k + 1) = x % 2 ^ k + (x.testBit k).toNat * 2 ^ k

One more bit of a remainder: the next binary digit, in the form the carry chain steps through.

theorem DescriptiveComplexity.BitSum.mod_two_pow_eq_sum (x m : ℕ) : x % 2 ^ m = ∑ i ∈ Finset.range m, (x.testBit i).toNat * 2 ^ i

A number is the sum of its bits, below any width that bounds it.

theorem DescriptiveComplexity.BitSum.eq_sum_testBit {x m : ℕ} (hx : x < 2 ^ m) : x = ∑ i ∈ Finset.range m, (x.testBit i).toNat * 2 ^ i

The same, for a number known to fit.

theorem DescriptiveComplexity.BitSum.lt_two_pow_of_high_bits {v k : ℕ} (h : ∀ (i : ℕ), k ≤ i → v.testBit i = false) : v < 2 ^ k

A number with no high bits is small: the converse of Nat.testBit_lt_two_pow, which the guessed elements' vanishing conditions are read through.

theorem DescriptiveComplexity.BitSum.eq_two_pow_mul_div {x b : ℕ} (hlow : ∀ i < b, x.testBit i = false) : x = 2 ^ b * (x / 2 ^ b)

A number with no low bits is a shifted quotient.

theorem DescriptiveComplexity.BitSum.eq_two_pow_mul_of_testBit {x t b : ℕ} (hlow : ∀ i < b, x.testBit i = false) (hbits : ∀ (k : ℕ), x.testBit (b + k) = t.testBit k) : x = 2 ^ b * t

A number whose bits are another's, shifted, is that number shifted: the identity that reads a certificate's tail element as 2 ^ b times its value.

Weighted sums of column ranges

def DescriptiveComplexity.BitSum.intervalSum (h : ℕ → ℕ) (a m : ℕ) : ℕ

The weighted sum of a range of columns: Σ_{t<m} h (a + t) · 2 ^ t, the value of the columns a, …, a + m - 1 read from position a.

Equations

• DescriptiveComplexity.BitSum.intervalSum h a m = ∑ t ∈ Finset.range m, h (a + t) * 2 ^ t

@[simp]

theorem DescriptiveComplexity.BitSum.intervalSum_zero (h : ℕ → ℕ) (a : ℕ) : intervalSum h a 0 = 0

theorem DescriptiveComplexity.BitSum.intervalSum_succ (h : ℕ → ℕ) (a m : ℕ) : intervalSum h a (m + 1) = intervalSum h a m + h (a + m) * 2 ^ m

One more column on top.

@[simp]

theorem DescriptiveComplexity.BitSum.intervalSum_one (h : ℕ → ℕ) (a : ℕ) : intervalSum h a 1 = h a

theorem DescriptiveComplexity.BitSum.intervalSum_append (h : ℕ → ℕ) (a m m' : ℕ) : intervalSum h a (m + m') = intervalSum h a m + 2 ^ m * intervalSum h (a + m) m'

Concatenating two ranges of columns: the second range enters shifted by the width of the first. Every regrouping below is this identity.

theorem DescriptiveComplexity.BitSum.intervalSum_lt {h : ℕ → ℕ} {a m H : ℕ} (hH : 0 < H) (hb : ∀ t < m, h (a + t) < H) : intervalSum h a m < H * 2 ^ m

The sum of a range fits just above the widest column.

The carry chain of one range

def DescriptiveComplexity.BitSum.carryChain (h : ℕ → ℕ) (a t : ℕ) : ℕ

The remainder after adding the columns up to a + t: what has been accumulated and not yet written, i.e., the partial sum shifted below its first unwritten position. The certificate stores these, one field per column.

Equations

• DescriptiveComplexity.BitSum.carryChain h a t = DescriptiveComplexity.BitSum.intervalSum h a (t + 1) / 2 ^ (t + 1)

theorem DescriptiveComplexity.BitSum.carryChain_lt {h : ℕ → ℕ} {a t H : ℕ} (hH : 0 < H) (hb : ∀ u < t + 1, h (a + u) < H) : carryChain h a t < H

The remainders stay small: below any bound on the columns.

theorem DescriptiveComplexity.BitSum.carryChain_base {h : ℕ → ℕ} {a m : ℕ} (hm : 0 < m) : h a = 2 * carryChain h a 0 + ((intervalSum h a m).testBit 0).toNat

The first column: it splits into the lowest bit of the sum and the first remainder.

theorem DescriptiveComplexity.BitSum.carryChain_step {h : ℕ → ℕ} {a m t : ℕ} (ht : t + 1 < m) : carryChain h a t + h (a + (t + 1)) = 2 * carryChain h a (t + 1) + ((intervalSum h a m).testBit (t + 1)).toNat

One step of the chain: the incoming remainder plus the next column splits into the next bit of the sum and the outgoing remainder. This is the equation the certificate checks at every boundary.

theorem DescriptiveComplexity.BitSum.carryChain_last {h : ℕ → ℕ} {a m : ℕ} (hm : 0 < m) : intervalSum h a m / 2 ^ m = carryChain h a (m - 1)

The final remainder is the high part: what is left after the last column is exactly the bits of the sum above the range.

Reading a packed element off its windows

theorem DescriptiveComplexity.BitSum.eq_packVal_of_windows {x w M : ℕ} {f : ℕ → ℕ} (hw : 0 < w) (hf : ∀ m < M, f m < 2 ^ w) (hwin : ∀ m < M, x / 2 ^ (m * w) % 2 ^ w = f m) (hhigh : ∀ (i : ℕ), M * w ≤ i → x.testBit i = false) : x = packVal w f M

An element whose windows are a packing's fields is the packing: equal windows at every field, no bits above, and the values fitting their fields pin the number bit by bit. This is how the soundness half reads the two half-sums off the guessed elements.

theorem DescriptiveComplexity.BitSum.packVal_evenOdd (h : ℕ → ℕ) (g M : ℕ) : packVal (2 * g) (fun (m : ℕ) => intervalSum h (m * (2 * g)) g) M + 2 ^ g * packVal (2 * g) (fun (m : ℕ) => intervalSum h (m * (2 * g) + g) g) M = intervalSum h 0 (M * (2 * g))

Re-assembling the two half-sums: the packing of the even block sums plus the packing of the odd ones, shifted by one block, is the weighted sum of all the columns they cover. This is the identity behind the one addition of the certificate.

The columns of a product

noncomputable def DescriptiveComplexity.BitSum.colWordN (x y j : ℕ) : ℕ

The word of one column: its bit at i says that y has a one at i and x a one at j - i – a pair of set bits whose indices add to j. It is a sub-mask of y, so it is always the value of an element.

Equations

• DescriptiveComplexity.BitSum.colWordN x y j = y &&& DescriptiveComplexity.bitsVal (fun (i : ℕ) => decide (i ≤ j) && x.testBit (j - i)) (j + 1)

theorem DescriptiveComplexity.BitSum.testBit_colWordN (x y j i : ℕ) : (colWordN x y j).testBit i = (y.testBit i && (decide (i ≤ j) && x.testBit (j - i)))

What the bits of a column word are.

theorem DescriptiveComplexity.BitSum.colWordN_le (x y j : ℕ) : colWordN x y j ≤ y

A column word is a sub-mask of y.

noncomputable def DescriptiveComplexity.BitSum.colCountN (x y P j : ℕ) : ℕ

The count of one column: the number of ones of its word among the first P positions.

Equations

• DescriptiveComplexity.BitSum.colCountN x y P j = DescriptiveComplexity.BitSum.onesBelow (DescriptiveComplexity.BitSum.colWordN x y j) P

theorem DescriptiveComplexity.BitSum.colCountN_le (x y P j : ℕ) : colCountN x y P j ≤ P

A column has no more ones than there are positions.

theorem DescriptiveComplexity.BitSum.mul_eq_colSum {x y P : ℕ} (hx : x < 2 ^ P) (hy : y < 2 ^ P) (hover : ∀ (i d : ℕ), y.testBit i = true → x.testBit d = true → i + d < P) : x * y = intervalSum (colCountN x y P) 0 P

The product is the weighted sum of its column counts – the schoolbook multiplication, columns grouped by weight, under the one condition that no pair of set bits reaches past the available positions.