Static preprocessing of a whole fusion tree

Every eligible large-width internal node stores the words of its actual classically chosen NodeParameters. All other parameter words are zero. Child minima inherit strict ordering and full-key bounds from the leaves. Consequently the concrete contiguous encoding needs no assumed preprocessing header or node-search oracle.

This is a classical static construction. It asserts no RAM preprocessing time, and does not compose the node query with whole-tree traversal or the small-width binary fallback.

Main definitions

• childMinima: the full keys used by an internal fusion-node query.
• ParameterEligible: the actual hypotheses needed to choose fitting node parameters.
• parameterWords: one total parameter assignment for the whole tree at each word width.

Main results

• childMinima_strictMono, childMinima_fit: leaf invariants imply node-key invariants.
• parameterWords_node: the exact chosen witness used in each eligible node header.
• parameterWords_fit: every parameter word fits, even for invalid trees and zero width.
• preprocessed_contentFits: valid trees with bounded leaves have fitting contents.
• preprocessed_encoding_exists: concrete memory, decoding and at most 126n + 18 words.

References

• [FW93]

theorem Cslib.Algorithms.WordRAM.FusionTree.minimum_mem {B : ℕ} {t : Lean.FusionTree.Tree} (ht : Lean.FusionTree.Tree.Valid B t) (hne : t.keys ≠ []) : t.minimum ∈ t.keys

A nonempty valid tree's cached minimum is one of its actual leaf keys.

def Cslib.Algorithms.WordRAM.FusionTree.childMinima (cs : List Lean.FusionTree.Tree) : Fin cs.length → ℕ

Full cached child minima, in the same order as the interleaved child table.

theorem Cslib.Algorithms.WordRAM.FusionTree.childMinima_mem {B m : ℕ} {cs : List Lean.FusionTree.Tree} (ht : Lean.FusionTree.Tree.Valid B (Lean.FusionTree.Tree.node m cs)) (i : Fin cs.length) : childMinima cs i ∈ cs[i].keys

Each valid nonempty child supplies an actual leaf key to the node's query table.

theorem Cslib.Algorithms.WordRAM.FusionTree.childMinima_strictMono {B m : ℕ} {cs : List Lean.FusionTree.Tree} (ht : Lean.FusionTree.Tree.Valid B (Lean.FusionTree.Tree.node m cs)) (hs : List.Pairwise (fun (x1 x2 : ℕ) => x1 < x2) (Lean.FusionTree.Tree.node m cs).keys) : StrictMono (childMinima cs)

Sorted distinct leaves imply strictly increasing full child minima.

theorem Cslib.Algorithms.WordRAM.FusionTree.childMinima_fit {B w m : ℕ} {cs : List Lean.FusionTree.Tree} (ht : Lean.FusionTree.Tree.Valid B (Lean.FusionTree.Tree.node m cs)) (hb : ∀ x ∈ (Lean.FusionTree.Tree.node m cs).keys, WordRAM.Fits w x) (i : Fin cs.length) : WordRAM.Fits w (childMinima cs i)

Every child minimum obeys the full-key bound on the leaves.

def Cslib.Algorithms.WordRAM.FusionTree.ParameterEligible (w : ℕ) (cs : List Lean.FusionTree.Tree) : Prop

Eligibility checks real width, occupancy, ordering and full-key bounds. Small-width binary nodes need no fusion parameters.

noncomputable def Cslib.Algorithms.WordRAM.FusionTree.parameterWords (w : ℕ) : Parameters

One uniform static assignment for all trees. Leaves and ineligible nodes have fifteen zero parameter words. The remaining three header words are supplied by encode.

theorem Cslib.Algorithms.WordRAM.FusionTree.parameterWords_node {w m : ℕ} {cs : List Lean.FusionTree.Tree} (h : ParameterEligible w cs) : parameterWords w (Lean.FusionTree.Tree.node m cs) = (NodeParameters.choose ⋯ ⋯ ⋯ ⋯ ⋯).words

Exact agreement with the chosen node witness, with no header-correctness hypothesis.

theorem Cslib.Algorithms.WordRAM.FusionTree.parameterWords_leaf (w : ℕ) (xs : List ℕ) : parameterWords w (Lean.FusionTree.Tree.leaf xs) = fun (x : Fin 15) => 0

Leaves use no fusion parameters, including empty and singleton leaves.

theorem Cslib.Algorithms.WordRAM.FusionTree.parameterWords_small {w : ℕ} (hw : ¬9 ≤ Nat.log 2 w) (m : ℕ) (cs : List Lean.FusionTree.Tree) : parameterWords w (Lean.FusionTree.Tree.node m cs) = fun (x : Fin 15) => 0

Small-width internal nodes use no fusion parameters.

theorem Cslib.Algorithms.WordRAM.FusionTree.parameterWords_fit (w : ℕ) (t : Lean.FusionTree.Tree) (j : Fin 15) : WordRAM.Fits w (parameterWords w t j)

All parameter words fit for every tree and width, independently of validity.

theorem Cslib.Algorithms.WordRAM.FusionTree.parameterEligible_of_valid {w m : ℕ} {cs : List Lean.FusionTree.Tree} (hw : 9 ≤ Nat.log 2 w) (ht : Lean.FusionTree.Tree.Valid (Lean.FusionTree.branching w) (Lean.FusionTree.Tree.node m cs)) (hs : List.Pairwise (fun (x1 x2 : ℕ) => x1 < x2) (Lean.FusionTree.Tree.node m cs).keys) (hb : ∀ x ∈ (Lean.FusionTree.Tree.node m cs).keys, WordRAM.Fits w x) : ParameterEligible w cs

Every large-width valid ordered bounded node is eligible for actual preprocessing.

theorem Cslib.Algorithms.WordRAM.FusionTree.preprocessed_contentFits {B w : ℕ} {t : Lean.FusionTree.Tree} (ht : Lean.FusionTree.Tree.Valid B t) (hb : ∀ x ∈ t.keys, WordRAM.Fits w x) : ContentFits w (parameterWords w) t

Valid trees with bounded leaves have fitting cached minima and actual parameters. Ordering is unnecessary for this fit statement because eligibility checks it itself.

theorem Cslib.Algorithms.WordRAM.FusionTree.preprocessed_contentFits_build (w : ℕ) (xs : List ℕ) (hb : ∀ x ∈ xs, WordRAM.Fits w x) : ContentFits w (parameterWords w) (Lean.FusionTree.Tree.build (Lean.FusionTree.branching w) xs)

The built tree has fitting actual preprocessing contents from full-key bounds alone.

theorem Cslib.Algorithms.WordRAM.FusionTree.preprocessed_encoding_exists {w base : ℕ} (xs : List ℕ) (hb : ∀ x ∈ xs, WordRAM.Fits w x) (ha : ArenaFits w base (Lean.FusionTree.Tree.build (Lean.FusionTree.branching w) xs)) : ∃ (mem : ℕ → ℕ), Rep (parameterWords w) (Lean.FusionTree.Tree.build (Lean.FusionTree.branching w) xs) base mem ∧ (∀ (a : ℕ), WordRAM.Fits w (mem a)) ∧ decode ((Lean.FusionTree.Tree.build (Lean.FusionTree.branching w) xs).height + 1) mem base = Lean.FusionTree.Tree.build (Lean.FusionTree.branching w) xs ∧ (encode (parameterWords w) base (Lean.FusionTree.Tree.build (Lean.FusionTree.branching w) xs)).length ≤ 126 * xs.length + 18

A concrete whole-tree memory with actual chosen preprocessing, exact decoding and linear allocated words. The arena frontier is explicit; fitting keys alone do not bound it. For unsorted inputs ineligible nodes receive zeros; ordered inputs additionally satisfy parameterEligible_of_valid at every large-width internal node. No query or RAM preprocessing-time certificate is asserted.