Slot-packed natural numbers

packN W d n = Σ_{j < n} d j · 2^(W j). When every digit is below 2^W, bitwise and, shifts, slot-wise sums and differences, and horizontal sums (mod 2^W - 1) act digit by digit.

def Cayley.Pack.packN (W : ℕ) (d : ℕ → ℕ) : ℕ → ℕ

Σ_{j < n} d j · 2^(W j).

Equations

• Cayley.Pack.packN W d 0 = 0
• Cayley.Pack.packN W d n.succ = Cayley.Pack.packN W d n + d n * 2 ^ (W * n)

theorem Cayley.Pack.packN_succ {W : ℕ} {d : ℕ → ℕ} (n : ℕ) : packN W d (n + 1) = packN W d n + d n * 2 ^ (W * n)

theorem Cayley.Pack.packN_eq_sum {W : ℕ} {d : ℕ → ℕ} {n : ℕ} : packN W d n = ∑ j ∈ Finset.range n, d j * 2 ^ (W * j)

theorem Cayley.Pack.packN_lt {W : ℕ} {d : ℕ → ℕ} {n : ℕ} (hd : ∀ j < n, d j < 2 ^ W) : packN W d n < 2 ^ (W * n)

theorem Cayley.Pack.testBit_packN {W : ℕ} {d : ℕ → ℕ} {n : ℕ} (hd : ∀ j < n, d j < 2 ^ W) (k : ℕ) : (packN W d n).testBit k = (decide (k < W * n) && (d (k / W)).testBit (k % W))

theorem Cayley.Pack.packN_land {W : ℕ} {d e : ℕ → ℕ} {n : ℕ} (hd : ∀ j < n, d j < 2 ^ W) (he : ∀ j < n, e j < 2 ^ W) : packN W d n &&& packN W e n = packN W (fun (j : ℕ) => d j &&& e j) n

theorem Cayley.Pack.packN_add {W : ℕ} {d e : ℕ → ℕ} {n : ℕ} : packN W (fun (j : ℕ) => d j + e j) n = packN W d n + packN W e n

theorem Cayley.Pack.packN_sub {W : ℕ} {d e : ℕ → ℕ} {n : ℕ} (h : ∀ j < n, e j ≤ d j) : packN W (fun (j : ℕ) => d j - e j) n = packN W d n - packN W e n

theorem Cayley.Pack.packN_mul_left {W : ℕ} {d : ℕ → ℕ} {n : ℕ} (c : ℕ) : c * packN W d n = packN W (fun (j : ℕ) => c * d j) n

theorem Cayley.Pack.packN_congr {W : ℕ} {d e : ℕ → ℕ} {n : ℕ} (h : ∀ j < n, d j = e j) : packN W d n = packN W e n

theorem Cayley.Pack.packN_land_low {W : ℕ} {d : ℕ → ℕ} {n : ℕ} (hd : ∀ j < n, d j < 2 ^ W) (hn : 0 < n) : packN W d n &&& 2 ^ W - 1 = d 0

Slot 0 of a packed number.

theorem Cayley.Pack.packN_signs {W : ℕ} {d : ℕ → ℕ} {n : ℕ} (hW : 0 < W) (hd : ∀ j < n, d j < 2 ^ W) : packN W d n >>> (W - 1) &&& packN W (fun (x : ℕ) => 1) n = packN W (fun (j : ℕ) => d j / 2 ^ (W - 1)) n

The top bit of every slot, moved to the slot's bottom.

theorem Cayley.Pack.packN_mod {W : ℕ} {d : ℕ → ℕ} {n : ℕ} (hd : ∑ j ∈ Finset.range n, d j < 2 ^ W - 1) : packN W d n % (2 ^ W - 1) = ∑ j ∈ Finset.range n, d j

Horizontal sum: 2^W ≡ 1 [MOD 2^W - 1].