Counting packed Boolean fields by multiplication

Multiplying packed zero-or-one fields by an all-ones radix word places their sum in the middle field. A radix larger than the number of fields prevents all carries. This is an arithmetic identity; a RAM client must separately justify product overflow.

Main results

• countPackedFlags: multiplication, division, and remainder recover the number of set fields.

References

• Fredman and Willard, Surpassing the information theoretic bound with fusion trees.

theorem Cslib.BitString.countPackedFlags {base n : ℕ} (f : ℕ → Bool) (hn : 0 < n) (hb : n < base) : ((packRadix base n fun (i : ℕ) => (f i).toNat) * packRadix base n fun (x : ℕ) => 1) / base ^ (n - 1) % base = ∑ i ∈ Finset.range n, (f i).toNat

With fewer fields than the radix, the middle digit of this product counts all set fields. The product itself can occupy twice the original packed width.