Always-Correct Succinct Dynamic Fusion Nodes Are Impossible: A Cell-Probe Lower Bound in the Small-Set, Large-Universe Regime
Ian D'Ambrosio
cs.DS
Aug 22, 2026 · v1
cs.CC
TL;DR
The full cell-probe lower bound proof, including memory model, hard distribution, communication bounds and corollaries, is formalized and kernel-checked in Lean 4 with Mathlib.
Abstract
Kuszmaul, Liang, and Zhou (SODA 2026) ask whether succinct constant-time dynamic fusion nodes exist when the number of stored keys is polylogarithmic in the universe size. We give a negative answer for always-correct structures. For n^8 <= U, log_2 U >= 2^70, and redundancy 0 <= R < n, a dynamic dictionary requires at least 2^-26 log_2(1+n/(R+1)) expected-amortized cell probes per operation. The model permits fixed layouts of packed cells of at most one word each, including the short-spill convention used by succinct word-RAM structures, and covers zero-error Las Vegas algorithms with fresh per-invocation randomness and almost-sure termination. The proof repairs a conditioning defect in the inherited communication argument by placing pointwise probe caps inside the consistency event, then extends the lower bound to large universes through a scale-adaptive entropy parameter. Consequently, when U=2^w and n=ceil(w^c) for any fixed c>0, no always-correct predecessor structure can use log_2 binom(U,n)+o(n) persistent mutable bits and support constant-time operations. Constant expected-amortized time requires Omega(n) redundant bits. Lean 4 checks the complete packed-memory and fresh-random indexed models, hard distribution, communication bounds, separator, nested-forest accounting, deterministic and Las Vegas lower bounds, strict-predecessor reduction, and redundancy corollaries.
Problem
Kuszmaul, Liang, and Zhou asked whether succinct constant-time dynamic fusion nodes exist when the number of keys is polylogarithmic in the universe size. A prior dynamic-dictionary lower bound by Li, Liang, Yu, and Zhou covered only polynomial universes.
Approach
The authors prove a cell-probe lower bound for always-correct deterministic and Las Vegas dynamic dictionaries in a fixed-layout packed-cell model. They repair a conditioning defect in the inherited inner communication game by placing pointwise probe caps inside the consistency event. They extend the bound to large universes with a scale-adaptive entropy parameter, and they add tree accounting over nested forests and a public-coin Bloomier-style separator. The whole argument is formalized operationally in Lean 4 against a pinned Mathlib revision, with audit files mapping paper claims to Lean declarations.
Results
For n^8 <= U, log U >= 2^70 and redundancy R < n, every always-correct dictionary needs at least 2^-26 log(1+n/(R+1)) expected-amortized probes per operation. Consequently, no succinct constant-time predecessor structure exists for n = ceil(w^c), and constant expected-amortized time requires Omega(n) redundant bits. All of these results are checked by the Lean kernel.
