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 #

Weighted sums of column ranges #

source

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

Instances For

Dependency graph

source

@[simp]

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

intervalSum h a 0 = 0

Dependency graph

source

@[simp]

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

intervalSum h a 1 = h a

Dependency graph

source

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.

Dependency graph

The carry chain of one range #

source

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)

Instances For

Dependency graph

source

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.

Dependency graph

source

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.

Dependency graph

source

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.

Dependency graph

Reading a packed element off its windows #

source

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.

Dependency graph

source

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.

Dependency graph