Word-size-dependent fusion-tree capacity

A power-of-two branching factor leaves explicit slack for checked arithmetic. Above width 512, 16B⁵ ≤ w; below that threshold the branching factor is two. In both regimes the constructed tree has height at most 14 (1 + log_w n), with one constant for all widths. These are arithmetic and tree-height bounds, not an instruction-count certificate.

Main definitions

• branching: the chosen capacity, always at least two.

Main results

• branching_capacity: quantitative room for packed sketches at large widths.
• height_build_branching_le: the desired word-logarithmic height bound.
• packed_width_le: both packed-comparison products fit a physical word.

References

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

def Cslib.Algorithms.Lean.FusionTree.branching (w : ℕ) : ℕ

Below width 512, binary branching suffices up to a uniform constant. At larger widths, the exponent leaves four bits of slack for the fifth-power capacity bound.

theorem Cslib.Algorithms.Lean.FusionTree.two_le_branching (w : ℕ) : 2 ≤ branching w

theorem Cslib.Algorithms.Lean.FusionTree.branching_capacity {w : ℕ} (hw : 9 ≤ Nat.log 2 w) : 16 * branching w ^ 5 ≤ w

Large-width nodes have slack for compression and both rank multiplications.

theorem Cslib.Algorithms.Lean.FusionTree.word_le_branching_pow (w : ℕ) : w ≤ branching w ^ 14

One comparison of bases works uniformly in the small- and large-width regimes.

theorem Cslib.Algorithms.Lean.FusionTree.height_build_branching_le {w : ℕ} (hw : 2 ≤ w) (xs : List ℕ) : (Tree.build (branching w) xs).height ≤ 14 * (Nat.log w xs.length + 1)

A single constant bounds the constructed tree's word-logarithmic height, including empty and singleton inputs. Predecessor runtime still requires a constant-time node implementation.

theorem Cslib.Algorithms.Lean.FusionTree.packed_width_le {w n r : ℕ} (hw : 9 ≤ Nat.log 2 w) (hn : n ≤ branching w) (hr : r ≤ branching w) : 2 * ((2 * r ^ 4 + 1) * n) ≤ w

At large widths, a node with at most B keys and at most B relevant bits has enough room for fields of width 2r⁴+1 and the complete count product.

theorem Cslib.Algorithms.Lean.FusionTree.compression_window_le {w n r : ℕ} (hw : 9 ≤ Nat.log 2 w) (hn0 : 0 < n) (hn : n ≤ branching w) (hr : r ≤ branching w) : 2 * r ^ 4 + (w - 2 * (w / 2)) ≤ w / 2

The same packed-width slack puts the entire compressed window in a single product limb.