Static fusion trees for finite sets

Every finite set of distinct unsigned word keys has a static fusion-tree representation. Preprocessing sorts the set, builds the tree, and chooses its proved compression parameters; no RAM preprocessing-time bound is claimed. Query execution uses the actual standard-basis program, whose bounded-size nonuniform code family depends only on physical word width.

The explicit arena contract covers the whole allocation frontier, in addition to the keys and query fitting words. The returned option is two words: presence in register 32 and a key in register 33. This distinguishes absence from key zero without requiring an extra data bit.

Main definitions

• Static.tree: the tree constructed from an arbitrary finite set.
• Static.initial: its actual preprocessed memory and query registers.
• Static.IsPredecessor: conventional inclusive predecessor semantics.
• Static.workingWords: allocated data words plus all 1024 query registers.

Main results

• Static.query_spec: actual halting RAM execution in 3100000 (1 + log_w n) instructions.
• Static.workingWords_le: at most 126n + 1042 data and register words.
• Static.workingWords_le_of_nonempty: at most 1168n words for nonempty sets.

References

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

def Cslib.Algorithms.WordRAM.FusionTree.Static.orderedKeys (s : Finset ℕ) : List ℕ

Sorting is part of static preprocessing; queries do not scan this list.

def Cslib.Algorithms.WordRAM.FusionTree.Static.tree (w : ℕ) (s : Finset ℕ) : Lean.FusionTree.Tree

The concrete tree for a finite key set.

noncomputable def Cslib.Algorithms.WordRAM.FusionTree.Static.initial (w : ℕ) (s : Finset ℕ) (base q : ℕ) : WordRAM.Data QueryProgram.registers

Preprocessed memory, query, and base address, with zero initial workspace registers.

def Cslib.Algorithms.WordRAM.FusionTree.Static.IsPredecessor (s : Finset ℕ) (q : ℕ) : Option ℕ → Prop

Conventional inclusive predecessor, with a separate case for absence.

def Cslib.Algorithms.WordRAM.FusionTree.Static.workingWords (w : ℕ) (s : Finset ℕ) : ℕ

All allocated data and working registers. The compiled program has a separate uniform size bound of 201051 instructions, including halt; it contains the width-only constants.

theorem Cslib.Algorithms.WordRAM.FusionTree.Static.workingWords_le (w : ℕ) (s : Finset ℕ) : workingWords w s ≤ 126 * s.card + 1042

A uniform linear bound, including the empty structure and all query registers.

theorem Cslib.Algorithms.WordRAM.FusionTree.Static.workingWords_le_of_nonempty (w : ℕ) {s : Finset ℕ} (hs : s.Nonempty) : workingWords w s ≤ 1168 * s.card

For nonempty sets, the additive workspace and empty-root constants are absorbed in n.

theorem Cslib.Algorithms.WordRAM.FusionTree.Static.arenaFits_of_bound {w base : ℕ} (s : Finset ℕ) (ha : WordRAM.Fits w (base + 126 * s.card + 18)) : ArenaFits w base (tree w s)

A sufficient input-size-only address condition for the actual allocation.

theorem Cslib.Algorithms.WordRAM.FusionTree.Static.query_spec {w base q : ℕ} (s : Finset ℕ) (hw : 2 ≤ w) (hk : ∀ k ∈ s, WordRAM.Fits w k) (ha : ArenaFits w base (tree w s)) (hq : WordRAM.Fits w q) : WordRAM.Data.Bounded w (initial w s base q) ∧ workingWords w s ≤ 126 * s.card + 1042 ∧ ∃ (y : WordRAM.Data QueryProgram.registers) (k : ℕ), k + 1 ≤ 3100000 * (Nat.log w s.card + 1) ∧ WordRAM.Runs w (QueryProgram.program w) { pc := 0, data := initial w s base q } { pc := (QueryProgram.code w).size, data := y } k ∧ WordRAM.Executes w (QueryProgram.program w) { pc := 0, data := initial w s base q } (y.regs QueryProgram.value) (k + 1) ∧ IsPredecessor s q (QueryProgram.answer y) ∧ y.mem = (initial w s base q).mem ∧ y.regs QueryProgram.query = q

Every arbitrary finite key set receives an actual bounded RAM representation and correct halting predecessor execution. Time includes initialization, all node instructions, traversal, and halt. Space includes the allocated records, auxiliary data, and all working registers. Width selects the code family; the key set, address, and query are runtime data.