Concrete fusion-node preprocessing parameters

Static preprocessing chooses collision-free shifts and three half-word multiplier digits. All other stored constants are explicit arithmetic expressions in these witnesses and the stored keys. The choices have no preprocessing-time certificate. Arithmetic compression agrees with perfect-sketch comparisons on all inputs; full-key query correction and the complete fusion-tree query remain separate.

Main definitions

• NodeParameters: actual compression witnesses for a node.
• NodeParameters.words: fifteen physical parameter words, independent of the node header.

Main results

• NodeParameters.exists_parameters: witnesses for every large-width bounded sorted node.
• NodeParameters.compressed_lt_iff: comparison agreement for arbitrary inputs.
• NodeParameters.words_fit: every stored parameter fits the physical word.

References

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

def Cslib.Algorithms.WordRAM.FusionTree.relevantCount {n : ℕ} (w : ℕ) (keys : Fin n → ℕ) : ℕ

Number of selected source positions.

def Cslib.Algorithms.WordRAM.FusionTree.sourcePositions {n : ℕ} (w : ℕ) (keys : Fin n → ℕ) : Fin (relevantCount w keys) ↪o ℕ

Source positions enumerated in increasing significance order.

theorem Cslib.Algorithms.WordRAM.FusionTree.sourcePositions_list {n : ℕ} (w : ℕ) (keys : Fin n → ℕ) : List.ofFn ⇑(sourcePositions w keys) = (Lean.FusionTree.relevantBits w keys).sort fun (x1 x2 : ℕ) => x1 ≤ x2

The source-position list is exactly the list defining the perfect sketch.

structure Cslib.Algorithms.WordRAM.FusionTree.NodeParameters (w : ℕ) {n : ℕ} (keys : Fin n → ℕ) : Type

Explicit compression witnesses. Correctness and word bounds below are derived from the collision, ordering and span properties supplied by the constructive shift theorem.

• shifts : Fin (relevantCount w keys) → ℕ

  Collision-free shift positions.

• cross_injective : Function.Injective fun (p : Fin (relevantCount w keys) × Fin (relevantCount w keys)) => (sourcePositions w keys) p.1 + self.shifts p.2

  Distinct cross terms prevent carries.

• diagonal_strictMono : StrictMono fun (i : Fin (relevantCount w keys)) => (sourcePositions w keys) i + self.shifts i

  Retained terms occur in significance order.

• span (i : Fin (relevantCount w keys)) : w < (sourcePositions w keys) i + self.shifts i ∧ (sourcePositions w keys) i + self.shifts i < w + 2 * relevantCount w keys ^ 4

  All retained terms lie in the short window.

• digits : Fin 3 → ℕ

  The three little-endian half-word digits of the multiplier.

• digits_lt (i : Fin 3) : self.digits i < WordRAM.Multiword.radix w

  Each multiplier digit fits the multiplication radix.

• digits_value : Nat.ofDigits (WordRAM.Multiword.radix w) (List.ofFn self.digits) = Lean.FusionTree.positionMask self.shifts

  The digits represent the actual shift mask.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.NodeParameters.r {w n : ℕ} {keys : Fin n → ℕ} (_p : NodeParameters w keys) : ℕ

Selected-bit count, at most one per adjacent pair.

def Cslib.Algorithms.WordRAM.FusionTree.NodeParameters.b {w n : ℕ} {keys : Fin n → ℕ} (p : NodeParameters w keys) : ℕ

Compressed payload width.

def Cslib.Algorithms.WordRAM.FusionTree.NodeParameters.C {w n : ℕ} {keys : Fin n → ℕ} (_p : NodeParameters w keys) : ℕ

Input position mask.

def Cslib.Algorithms.WordRAM.FusionTree.NodeParameters.M {w n : ℕ} {keys : Fin n → ℕ} (p : NodeParameters w keys) : ℕ

Full multiplier, represented in storage by three digits.

def Cslib.Algorithms.WordRAM.FusionTree.NodeParameters.D {w n : ℕ} {keys : Fin n → ℕ} (p : NodeParameters w keys) : ℕ

Retained output mask.

def Cslib.Algorithms.WordRAM.FusionTree.NodeParameters.compressed {w n : ℕ} {keys : Fin n → ℕ} (p : NodeParameters w keys) (x : ℕ) : ℕ

Arithmetic compressed sketch, for any natural input.

def Cslib.Algorithms.WordRAM.FusionTree.NodeParameters.sketches {w n : ℕ} {keys : Fin n → ℕ} (p : NodeParameters w keys) (i : ℕ) : ℕ

Stored sketches, extended by the sketch of zero outside the node.

def Cslib.Algorithms.WordRAM.FusionTree.NodeParameters.copies {w n : ℕ} {keys : Fin n → ℕ} (p : NodeParameters w keys) : ℕ

Query replication multiplier.

def Cslib.Algorithms.WordRAM.FusionTree.NodeParameters.packed {w n : ℕ} {keys : Fin n → ℕ} (p : NodeParameters w keys) : ℕ

Guarded original sketches.

def Cslib.Algorithms.WordRAM.FusionTree.NodeParameters.packedComplement {w n : ℕ} {keys : Fin n → ℕ} (p : NodeParameters w keys) : ℕ

Guarded complemented sketches.

def Cslib.Algorithms.WordRAM.FusionTree.NodeParameters.guards {w n : ℕ} {keys : Fin n → ℕ} (p : NodeParameters w keys) : ℕ

Guard mask for packed comparisons.

def Cslib.Algorithms.WordRAM.FusionTree.NodeParameters.middle {w n : ℕ} {keys : Fin n → ℕ} (p : NodeParameters w keys) : ℕ

Divisor selecting the middle count digit.

def Cslib.Algorithms.WordRAM.FusionTree.NodeParameters.radix {w n : ℕ} {keys : Fin n → ℕ} (p : NodeParameters w keys) : ℕ

Packed-field radix, distinct from the half-word multiplication radix.

def Cslib.Algorithms.WordRAM.FusionTree.NodeParameters.maximum {w n : ℕ} {keys : Fin n → ℕ} (p : NodeParameters w keys) : ℕ

Largest compressed payload.

theorem Cslib.Algorithms.WordRAM.FusionTree.NodeParameters.r_le {w n : ℕ} {keys : Fin n → ℕ} (p : NodeParameters w keys) : p.r ≤ n - 1

theorem Cslib.Algorithms.WordRAM.FusionTree.NodeParameters.diagonal_strictMono_sub {w n : ℕ} {keys : Fin n → ℕ} (p : NodeParameters w keys) : StrictMono fun (i : Fin (relevantCount w keys)) => (sourcePositions w keys) i + p.shifts i - w

theorem Cslib.Algorithms.WordRAM.FusionTree.NodeParameters.D_lt {w n : ℕ} {keys : Fin n → ℕ} (p : NodeParameters w keys) : p.D < 2 ^ p.b

theorem Cslib.Algorithms.WordRAM.FusionTree.NodeParameters.M_lt {w n : ℕ} {keys : Fin n → ℕ} (p : NodeParameters w keys) : p.M < 2 ^ (w + p.b)

The entire multiplier may exceed one word but fits in w + b bits.

theorem Cslib.Algorithms.WordRAM.FusionTree.NodeParameters.compressed_lt {w n : ℕ} {keys : Fin n → ℕ} (p : NodeParameters w keys) (x : ℕ) : p.compressed x < 2 ^ p.b

theorem Cslib.Algorithms.WordRAM.FusionTree.NodeParameters.compressed_lt_iff {w n : ℕ} {keys : Fin n → ℕ} (p : NodeParameters w keys) (x y : ℕ) : p.compressed x < p.compressed y ↔ BitString.sketch (Lean.FusionTree.relevantBits w keys) x < BitString.sketch (Lean.FusionTree.relevantBits w keys) y

The arithmetic sketch and the perfect sketch compare identically for all inputs, including inputs outside the stored key set and outside the physical word range.

theorem Cslib.Algorithms.WordRAM.FusionTree.NodeParameters.compressed_le_iff {w n : ℕ} {keys : Fin n → ℕ} (p : NodeParameters w keys) (x y : ℕ) : p.compressed x ≤ p.compressed y ↔ BitString.sketch (Lean.FusionTree.relevantBits w keys) x ≤ BitString.sketch (Lean.FusionTree.relevantBits w keys) y

Weak comparisons agree too, including equality queries.

theorem Cslib.Algorithms.WordRAM.FusionTree.NodeParameters.strictMono_compressed {w n : ℕ} {keys : Fin n → ℕ} (p : NodeParameters w keys) (hsorted : StrictMono keys) (hbound : ∀ (i : Fin n), keys i < 2 ^ w) : StrictMono fun (i : Fin n) => p.compressed (keys i)

The concrete stored arithmetic sketches remain strictly increasing.

theorem Cslib.Algorithms.WordRAM.FusionTree.NodeParameters.packed_width {w n : ℕ} {keys : Fin n → ℕ} (p : NodeParameters w keys) (hnB : n ≤ Lean.FusionTree.branching w) (hw : 9 ≤ Nat.log 2 w) : 2 * ((p.b + 1) * n) ≤ w

Capacity supplies the full packed-count multiplication bound.

theorem Cslib.Algorithms.WordRAM.FusionTree.NodeParameters.window {w n : ℕ} {keys : Fin n → ℕ} (p : NodeParameters w keys) (hn : 0 < n) (hnB : n ≤ Lean.FusionTree.branching w) (hw : 9 ≤ Nat.log 2 w) : p.b + (w - 2 * (w / 2)) ≤ w / 2

Capacity also supplies the odd-width-aware half-word extraction bound.

theorem Cslib.Algorithms.WordRAM.FusionTree.NodeParameters.C_fit {w n : ℕ} {keys : Fin n → ℕ} (p : NodeParameters w keys) (hsorted : StrictMono keys) (hbound : ∀ (i : Fin n), keys i < 2 ^ w) : WordRAM.Fits w p.C

theorem Cslib.Algorithms.WordRAM.FusionTree.NodeParameters.sketches_lt {w n : ℕ} {keys : Fin n → ℕ} (p : NodeParameters w keys) (i : ℕ) : p.sketches i < 2 ^ p.b

theorem Cslib.Algorithms.WordRAM.FusionTree.NodeParameters.count_lt_radix {w n : ℕ} {keys : Fin n → ℕ} (p : NodeParameters w keys) (hsorted : StrictMono keys) (hbound : ∀ (i : Fin n), keys i < 2 ^ w) : n < 2 ^ (p.b + 1)

Distinct perfect sketches give a numerical bound on the number of stored keys.

theorem Cslib.Algorithms.WordRAM.FusionTree.NodeParameters.count_fit {w n : ℕ} {keys : Fin n → ℕ} (p : NodeParameters w keys) (hn : 0 < n) (hsorted : StrictMono keys) (hbound : ∀ (i : Fin n), keys i < 2 ^ w) (hnB : n ≤ Lean.FusionTree.branching w) (hw : 9 ≤ Nat.log 2 w) : WordRAM.Fits w n

In particular the separately stored occupancy is a physical word.

theorem Cslib.Algorithms.WordRAM.FusionTree.NodeParameters.upperRank_eq {w n : ℕ} {keys : Fin n → ℕ} (p : NodeParameters w keys) (hn : 0 < n) (hsorted : StrictMono keys) (hbound : ∀ (i : Fin n), keys i < 2 ^ w) (q : ℕ) : upperRankExpr p.b n p.sketches (p.compressed q) = {i ∈ Finset.range n | BitString.sketch (Lean.FusionTree.relevantBits w keys) (if hi : i < n then keys ⟨i, hi⟩ else 0) ≤ BitString.sketch (Lean.FusionTree.relevantBits w keys) q}.card

The inclusive arithmetic rank counts perfect sketches at or below every query. This is a sketch rank, not the predecessor rank of the original keys.

theorem Cslib.Algorithms.WordRAM.FusionTree.NodeParameters.lowerRank_eq {w n : ℕ} {keys : Fin n → ℕ} (p : NodeParameters w keys) (hn : 0 < n) (hsorted : StrictMono keys) (hbound : ∀ (i : Fin n), keys i < 2 ^ w) (q : ℕ) : n - countGuards p.b n p.sketches (p.compressed q) = {i ∈ Finset.range n | BitString.sketch (Lean.FusionTree.relevantBits w keys) (if hi : i < n then keys ⟨i, hi⟩ else 0) < BitString.sketch (Lean.FusionTree.relevantBits w keys) q}.card

Strict arithmetic rank agrees with the perfect-sketch strict rank for every query, including zero and queries with the same sketch as a stored key.

def Cslib.Algorithms.WordRAM.FusionTree.NodeParameters.words {w n : ℕ} {keys : Fin n → ℕ} (p : NodeParameters w keys) : Fin 15 → ℕ

Slot order: input mask, three multiplier digits, retained mask, copies, complemented packed sketches, original packed sketches, guards, payload width, middle divisor, field radix, maximum payload, odd-width offset, selected-bit count. The node tag, occupancy and minimum belong to the separate three-word header.

theorem Cslib.Algorithms.WordRAM.FusionTree.NodeParameters.words_fit {w n : ℕ} {keys : Fin n → ℕ} (p : NodeParameters w keys) (hn : 2 ≤ n) (hsorted : StrictMono keys) (hbound : ∀ (i : Fin n), keys i < 2 ^ w) (hnB : n ≤ Lean.FusionTree.branching w) (hw : 9 ≤ Nat.log 2 w) (i : Fin 15) : WordRAM.Fits w (p.words i)

Every actual stored parameter is a physical word. The full multiplier is stored only as three digits, because its unbounded numeric value may exceed a physical word.

theorem Cslib.Algorithms.WordRAM.FusionTree.NodeParameters.exists_parameters {w n : ℕ} {keys : Fin n → ℕ} (hn : 2 ≤ n) (hsorted : StrictMono keys) (hbound : ∀ (i : Fin n), keys i < 2 ^ w) (hnB : n ≤ Lean.FusionTree.branching w) (hw : 9 ≤ Nat.log 2 w) : Nonempty (NodeParameters w keys)

Real preprocessing witnesses exist; no correctness or timing oracle is assumed.

noncomputable def Cslib.Algorithms.WordRAM.FusionTree.NodeParameters.choose {w n : ℕ} {keys : Fin n → ℕ} (hn : 2 ≤ n) (hsorted : StrictMono keys) (hbound : ∀ (i : Fin n), keys i < 2 ^ w) (hnB : n ≤ Lean.FusionTree.branching w) (hw : 9 ≤ Nat.log 2 w) : NodeParameters w keys

Static preprocessing explicitly uses classical choice; no preprocessing-time bound.