Static multiway predecessor trees

This is an outer multiway tree for fusion-tree search, independently of node search. Keys occur in leaves; each internal node caches the first key in its subtree. A node search may scan its children linearly. No word-RAM running-time bound is asserted here. Singleton branches are collapsed, so leaves need not all have the same depth.

Main definitions

• Tree: singleton leaves and internal nodes with cached subtree minima.
• Tree.build: executable construction from a list, with branching parameter B.
• Tree.predecessor: inclusive predecessor, using an explicit linear scan of child minima.

Main results

• Tree.keys_build, Tree.valid_build: construction preserves all keys and supplies occupancy.
• Tree.height_build_le: height is at most Nat.clog B n, uniformly for B ≥ 2.
• Tree.height_build_le_log_add_one: height is at most Nat.log B n + 1 for B ≥ 2.
• Tree.slots_build_le: keys, links, cached minima and headers occupy at most 14n + 2 slots.
• Tree.predecessor_build_eq_some_iff, Tree.predecessor_build_eq_none_iff: exact search semantics.

References

See [FW93] for fusion trees and their multiway outer search tree.

inductive Cslib.Algorithms.Lean.FusionTree.Tree : Type

A multiway tree representation. Well-formed leaves contain at most one key. The empty tree is represented by an empty leaf. Internal nodes store one cached minimum and their child pointers.

• leaf (keys : List ℕ) : Tree
• node (minimum : ℕ) (children : List Tree) : Tree

@[instance_reducible]

instance Cslib.Algorithms.Lean.FusionTree.instReprTree : Repr Tree

partial def Cslib.Algorithms.Lean.FusionTree.instReprTree.repr : Tree → ℕ → Std.Format

@[irreducible]

def Cslib.Algorithms.Lean.FusionTree.Tree.keys : Tree → List ℕ

Stored leaf keys in left-to-right order, without the cached internal minima.

def Cslib.Algorithms.Lean.FusionTree.Tree.minimum : Tree → ℕ

Cached subtree minimum, with zero used for an empty leaf.

@[irreducible]

def Cslib.Algorithms.Lean.FusionTree.Tree.height : Tree → ℕ

Height counts edges, so a leaf has height zero.

theorem Cslib.Algorithms.Lean.FusionTree.Tree.height_lt_node_of_mem {m : ℕ} {cs : List Tree} {t : Tree} (ht : t ∈ cs) : t.height < (node m cs).height

Every child has strictly smaller height than its parent node.

theorem Cslib.Algorithms.Lean.FusionTree.Tree.height_getElem_lt_node (m : ℕ) (cs : List Tree) (i : Fin cs.length) : cs[i].height < (node m cs).height

An indexed child has strictly smaller height than its parent node.

@[irreducible]

def Cslib.Algorithms.Lean.FusionTree.Tree.slots : Tree → ℕ

Structural storage in scalar slots, including the list representation: a leaf has a tag and a list reference; an internal node has a tag, minimum and child-list reference. Each list cell has a tag, an entry and a next link. A key is counted as one scalar, not by its bit length. There is no allocation of B slots at every node.

@[irreducible]

def Cslib.Algorithms.Lean.FusionTree.Tree.Valid (B : ℕ) : Tree → Prop

Occupancy and cached-minimum invariants. Every non-root child is nonempty.

def Cslib.Algorithms.Lean.FusionTree.Tree.join : List Tree → Tree

Form a node, collapsing groups of zero or one child.

def Cslib.Algorithms.Lean.FusionTree.Tree.chunks (B k : ℕ) (xs : List ℕ) : List (List ℕ)

Split into at most B consecutive nonempty blocks of at most k elements, using Mathlib's List.splitLengths. The caller must ensure that B * k covers the input.

def Cslib.Algorithms.Lean.FusionTree.Tree.buildAux (B : ℕ) : ℕ → List ℕ → Tree

Construct a tree of height at most h, for inputs of length at most B ^ h. Singleton child groups are collapsed, including on incomplete rightmost branches.

def Cslib.Algorithms.Lean.FusionTree.Tree.build (B : ℕ) (xs : List ℕ) : Tree

Construct a static tree. For 2 ≤ B, no input keys are lost, and the height is at most Nat.clog B xs.length. Sorting and distinctness are requirements for ordered search, not for construction or its shape bounds.

theorem Cslib.Algorithms.Lean.FusionTree.Tree.keys_join (cs : List Tree) : (join cs).keys = List.flatMap keys cs

theorem Cslib.Algorithms.Lean.FusionTree.Tree.chunks_length_le (B k : ℕ) (xs : List ℕ) : (chunks B k xs).length ≤ B

theorem Cslib.Algorithms.Lean.FusionTree.Tree.chunks_mem {B k : ℕ} {xs ys : List ℕ} (h : ys ∈ chunks B k xs) : ys ≠ [] ∧ ys.length ≤ k

theorem Cslib.Algorithms.Lean.FusionTree.Tree.flatten_chunks {B k : ℕ} {xs : List ℕ} (h : xs.length ≤ B * k) : (chunks B k xs).flatten = xs

theorem Cslib.Algorithms.Lean.FusionTree.Tree.keys_buildAux {B h : ℕ} {xs : List ℕ} (hn : xs.length ≤ B ^ h) : (buildAux B h xs).keys = xs

theorem Cslib.Algorithms.Lean.FusionTree.Tree.valid_join {B : ℕ} {cs : List Tree} (hl : cs.length ≤ B) (hc : ∀ (t : Tree), t ∈ cs → Valid B t ∧ t.keys ≠ []) : Valid B (join cs)

theorem Cslib.Algorithms.Lean.FusionTree.Tree.valid_buildAux {B h : ℕ} {xs : List ℕ} (hn : xs.length ≤ B ^ h) : Valid B (buildAux B h xs)

theorem Cslib.Algorithms.Lean.FusionTree.Tree.height_join_le {cs : List Tree} {h : ℕ} (hc : ∀ (t : Tree), t ∈ cs → t.height ≤ h) : (join cs).height ≤ h + 1

theorem Cslib.Algorithms.Lean.FusionTree.Tree.height_buildAux_le (B h : ℕ) (xs : List ℕ) : (buildAux B h xs).height ≤ h

theorem Cslib.Algorithms.Lean.FusionTree.Tree.keys_build {B : ℕ} (hB : 2 ≤ B) (xs : List ℕ) : (build B xs).keys = xs

Construction preserves the complete input list, including its order.

theorem Cslib.Algorithms.Lean.FusionTree.Tree.valid_build {B : ℕ} (hB : 2 ≤ B) (xs : List ℕ) : Valid B (build B xs)

Construction supplies the occupancy and cached-minimum invariants.

theorem Cslib.Algorithms.Lean.FusionTree.Tree.height_build_le (B : ℕ) (xs : List ℕ) : (build B xs).height ≤ Nat.clog B xs.length

The explicit height bound, uniform in the branching parameter.

theorem Cslib.Algorithms.Lean.FusionTree.Tree.height_build_le_log_add_one {B : ℕ} (hB : 2 ≤ B) (xs : List ℕ) : (build B xs).height ≤ Nat.log B xs.length + 1

A logarithmic height bound with a constant independent of the branching parameter.

theorem Cslib.Algorithms.Lean.FusionTree.Tree.slots_add_nine_le {B : ℕ} {t : Tree} (ht : Valid B t) (hne : t.keys ≠ []) : t.slots + 9 ≤ 14 * t.keys.length

Nonempty valid trees have storage bounded uniformly in their maximum node capacity.

theorem Cslib.Algorithms.Lean.FusionTree.Tree.slots_of_keys_eq_nil {B : ℕ} {t : Tree} (ht : Valid B t) (hne : t.keys = []) : t.slots = 2

Empty valid trees are empty leaves, with a tag and a reference to the empty list.

theorem Cslib.Algorithms.Lean.FusionTree.Tree.slots_build_le {B : ℕ} (hB : 2 ≤ B) (xs : List ℕ) : (build B xs).slots ≤ 14 * xs.length + 2

Total keys, child pointers, cached minima, node headers and list links use at most 14n+2 scalar slots. The numerical constant is independent of B. This is a structural bound, not a word-RAM heap encoding or a bit-space bound for unbounded natural numbers.

def Cslib.Algorithms.Lean.FusionTree.Tree.selectChild (q : ℕ) : List Tree → Option Tree

Linear semantic node search: select the last child whose cached minimum is at most q. Only the selected subtree is searched recursively.

theorem Cslib.Algorithms.Lean.FusionTree.Tree.selectChild_mem {q : ℕ} {cs : List Tree} {t : Tree} (h : selectChild q cs = some t) : t ∈ cs

def Cslib.Algorithms.Lean.FusionTree.Tree.listPredecessor (q : ℕ) : List ℕ → Option ℕ

Rightmost qualifying key in an input list. For sorted input this is inclusive predecessor.

@[irreducible]

def Cslib.Algorithms.Lean.FusionTree.Tree.predecessor (q : ℕ) : Tree → Option ℕ

Inclusive predecessor by cached-minimum routing, descending into at most one child per node. The linear node scan is explicit and is not charged as a constant-time operation.

theorem Cslib.Algorithms.Lean.FusionTree.Tree.minimum_eq_headD {B : ℕ} {t : Tree} (ht : Valid B t) : t.minimum = t.keys.headD 0

theorem Cslib.Algorithms.Lean.FusionTree.Tree.listPredecessor_eq_none_iff (q : ℕ) (xs : List ℕ) : listPredecessor q xs = none ↔ ∀ (x : ℕ), x ∈ xs → q < x

theorem Cslib.Algorithms.Lean.FusionTree.Tree.listPredecessor_append (q : ℕ) (xs ys : List ℕ) : listPredecessor q (xs ++ ys) = (listPredecessor q ys).or (listPredecessor q xs)

theorem Cslib.Algorithms.Lean.FusionTree.Tree.listPredecessor_ne_none_iff {q : ℕ} {xs : List ℕ} (hn : xs ≠ []) (hs : List.Pairwise (fun (x1 x2 : ℕ) => x1 ≤ x2) xs) : listPredecessor q xs ≠ none ↔ xs.headD 0 ≤ q

theorem Cslib.Algorithms.Lean.FusionTree.Tree.predecessor_eq_listPredecessor {B : ℕ} {t : Tree} (ht : Valid B t) (hs : List.Pairwise (fun (x1 x2 : ℕ) => x1 ≤ x2) t.keys) (q : ℕ) : predecessor q t = listPredecessor q t.keys

Cached-minimum routing agrees with rightmost list search on every valid ordered tree.

theorem Cslib.Algorithms.Lean.FusionTree.Tree.listPredecessor_some_spec {q p : ℕ} {xs : List ℕ} (hs : List.Pairwise (fun (x1 x2 : ℕ) => x1 ≤ x2) xs) (hp : listPredecessor q xs = some p) : p ∈ xs ∧ p ≤ q ∧ ∀ (x : ℕ), x ∈ xs → x ≤ q → x ≤ p

theorem Cslib.Algorithms.Lean.FusionTree.Tree.listPredecessor_eq_some_iff {q p : ℕ} {xs : List ℕ} (hs : List.Pairwise (fun (x1 x2 : ℕ) => x1 ≤ x2) xs) : listPredecessor q xs = some p ↔ p ∈ xs ∧ p ≤ q ∧ ∀ (x : ℕ), x ∈ xs → x ≤ q → x ≤ p

The list search returns exactly the greatest stored key not exceeding the query.

theorem Cslib.Algorithms.Lean.FusionTree.Tree.predecessor_build_eq_some_iff {B q p : ℕ} (hB : 2 ≤ B) {xs : List ℕ} (hs : List.Pairwise (fun (x1 x2 : ℕ) => x1 < x2) xs) : predecessor q (build B xs) = some p ↔ p ∈ xs ∧ p ≤ q ∧ ∀ (x : ℕ), x ∈ xs → x ≤ q → x ≤ p

Inclusive predecessor correctness for every sorted distinct input and every natural query.

theorem Cslib.Algorithms.Lean.FusionTree.Tree.predecessor_build_eq_none_iff {B q : ℕ} (hB : 2 ≤ B) {xs : List ℕ} (hs : List.Pairwise (fun (x1 x2 : ℕ) => x1 < x2) xs) : predecessor q (build B xs) = none ↔ ∀ (x : ℕ), x ∈ xs → q < x

Empty output is equivalent to having no stored key at or below the query.