Packing bounds for native multiplication

For every universe of size at least 257, eight words hold the carries at block boundaries, and sixteen words hold the carries of one block. The terminal column covers both input widths. Every bound applies to arbitrary universe sizes, including sizes between powers of two.

Main results

• Cslib.Logic.FO.Ordered.Multiplication.exists_parameters: uniform packing witnesses.

References

• N. Immerman, Descriptive Complexity, Theorem 1.17(1). These bounds support the carry-table variant of the source's packed short sums.

theorem Cslib.Logic.FO.Ordered.Multiplication.exists_parameters {n : ℕ} (hn : 257 ≤ n) : ∃ (h : ℕ) (e : ℕ) (m : ℕ), 2 ^ h ≤ n - 1 ∧ n - 1 < 2 ^ (h + 1) ∧ 8 ≤ h ∧ 16 * h < n ∧ e ≤ m ∧ 2 ^ e ≤ h ∧ h + 1 < 2 ^ 2 ^ e ∧ 2 * (h + 1) ≤ 2 ^ m ∧ 2 ^ m + 2 ^ e ≤ 8 * h ∧ (2 ^ e + 1) * 2 ^ e ≤ 16 * h

Powers of two give a block size and terminal column whose packed carries fit in a fixed number of words. The first pair characterizes the actual highest bit of n-1.