Binary multiplication columns and carries

Each multiplication column is a bitwise subword of the first input. Its number of set bits is the column's unnormalized coefficient. The weighted coefficients sum to the ordinary product; bounded carries normalize them to the product bits.

Main definitions

• Cslib.BitString.mulColumnWord: the contributing rows of one multiplication column.
• Cslib.BitString.mulColumn: its number of contributing rows.
• Cslib.BitString.mulPrefix: the weighted sum ∑ j < k, mulColumn x y j * 2 ^ j of the columns below k.
• Cslib.BitString.mulCarry: the actual carry entering a column.

Main results

• Cslib.BitString.mulColumnWord_le: each column word fits wherever the first input fits.
• Cslib.BitString.mulCarry_add_column: the exact arithmetic carry equation.
• Cslib.BitString.mul_eq_of_columns: zero-ended exact carry equations determine multiplication.

References

• N. Immerman, Descriptive Complexity, Theorem 1.17(1) and Lemma 1.18. This carry formulation supports a packed-block variant of the source's short-sum proof.

def Cslib.BitString.mulColumnWord (x y j : ℕ) : ℕ

The set bits record exactly the rows contributing to column j.

theorem Cslib.BitString.mulColumnWord_le (x y j : ℕ) : mulColumnWord x y j ≤ x

A column word is a subword of the first input, including in non-power-of-two universes.

theorem Cslib.BitString.mulColumnWord_testBit (x y j i : ℕ) : (mulColumnWord x y j).testBit i = true ↔ x.testBit i = true ∧ i ≤ j ∧ y.testBit (j - i) = true

The exact bitwise meaning of a multiplication column.

def Cslib.BitString.mulColumn (x y j : ℕ) : ℕ

The unnormalized coefficient of 2^j in binary multiplication.

theorem Cslib.BitString.mulColumn_le {x w : ℕ} (hx : x < 2 ^ w) (y j : ℕ) : mulColumn x y j ≤ w

At most one row per input bit contributes to a column.

def Cslib.BitString.mulPrefix (x y k : ℕ) : ℕ

The weighted contribution of all columns strictly below k.

def Cslib.BitString.mulCarry (x y k : ℕ) : ℕ

The carry entering column k, constructed from the actual lower columns.

@[simp]

theorem Cslib.BitString.mulCarry_zero (x y : ℕ) : mulCarry x y 0 = 0

No carry enters column 0.

theorem Cslib.BitString.mulCarry_add_column (x y k : ℕ) : mulCarry x y k + mulColumn x y k = ((x * y).testBit k).toNat + 2 * mulCarry x y (k + 1)

The actual carries satisfy the exact, nonmodular column equation.

theorem Cslib.BitString.mulCarry_le {x w : ℕ} (hx : x < 2 ^ w) (y k : ℕ) : mulCarry x y k ≤ w

Carries never exceed the number of available rows.

theorem Cslib.BitString.mulCarry_eq_zero {x y w k : ℕ} (hx : x < 2 ^ w) (hy : y < 2 ^ w) (hk : 2 * w ≤ k) : mulCarry x y k = 0

The terminal carry vanishes once the full product width is covered.

theorem Cslib.BitString.mul_eq_of_columns {x y z w k : ℕ} (hx : x < 2 ^ w) (hy : y < 2 ^ w) (hz : z < 2 ^ k) (hk : 2 * w ≤ k) (c : ℕ → ℕ) (hzero : c 0 = 0) (hend : c k = 0) (hstep : ∀ i < k, c i + mulColumn x y i = (z.testBit i).toNat + 2 * c (i + 1)) : x * y = z

Any exact zero-ended carry sequence determines ordinary multiplication.

theorem Cslib.BitString.mul_eq_of_blocks {x y z w k s : ℕ} (hx : x < 2 ^ w) (hy : y < 2 ^ w) (hz : z < 2 ^ k) (hk : 2 * w ≤ k) (hs : 0 < s) (hks : s ∣ k) (c : ℕ → ℕ) (hzero : c 0 = 0) (hend : c k = 0) (hblock : ∀ (q : ℕ), q * s < k → ∃ (a : ℕ → ℕ), a 0 = c (q * s) ∧ a s = c (q * s + s) ∧ ∀ t < s, a t + mulColumn x y (q * s + t) = (z.testBit (q * s + t)).toNat + 2 * a (t + 1)) : x * y = z

Blocks sharing their endpoint carries determine multiplication. The boundary sequence is global, while the interior witnesses may be chosen separately for every block.