Comparing multiplication-based and perfect fusion sketches

The gaps between the bits of an approximate sketch do not change comparisons. This holds for arbitrary queries as well as stored keys, and is separate from the subsequent correction needed to recover full-key predecessor ranks.

Main results

• approximateSketch_lt_iff_projectBits: approximate and perfect sketches give the same strict comparisons on every pair of inputs.

References

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

theorem Cslib.Algorithms.Lean.FusionTree.approximateSketch_lt_iff_projectBits {r w : ℕ} (b m : Fin r → ℕ) (h : Function.Injective fun (p : Fin r × Fin r) => b p.1 + m p.2) (hb : Function.Injective b) (hw : ∀ (i : Fin r), w ≤ b i + m i) (hs : StrictMono fun (i : Fin r) => b i + m i - w) (x y : ℕ) : approximateSketch w b m x < approximateSketch w b m y ↔ BitString.projectBits (List.ofFn b) x < BitString.projectBits (List.ofFn b) y

A collision-free multiplier with increasingly placed diagonal bits preserves every comparison made by the perfect sketch. The inputs need not belong to the stored key set.

theorem Cslib.Algorithms.Lean.FusionTree.exists_compression {r w : ℕ} (hr : 0 < r) (b : Fin r → ℕ) (hb : Function.Injective b) (hw : ∀ (i : Fin r), b i ≤ w) : ∃ (m : Fin r → ℕ), (Function.Injective fun (p : Fin r × Fin r) => b p.1 + m p.2) ∧ positionMask m < 2 ^ (w + 2 * r ^ 4) ∧ (∀ (x : ℕ), approximateSketch w b m x < 2 ^ (2 * r ^ 4)) ∧ ∀ (x y : ℕ), approximateSketch w b m x < approximateSketch w b m y ↔ BitString.projectBits (List.ofFn b) x < BitString.projectBits (List.ofFn b) y

Collision-free compression parameters exist for every nonempty set of distinct positions. The multiplier occupies at most w + 2r⁴ bits, and every compressed word at most 2r⁴. The construction preserves comparisons for all inputs. Preprocessing and multiword execution remain separate from this arithmetic existence theorem.