发表机构
Nth Research Collective（Nth研究集体）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本研究证明在键数量为宇宙大小多对数时，始终正确的简洁动态融合节点不存在，给出单元探针下界，并表明常数时间需 Omega(n) 冗余位。
AI 中文摘要
Kuszmaul、Liang 和 Zhou（SODA 2026）提出一个问题：当存储的键数量在宇宙大小的多对数范围内时，是否存在简洁的常数时间动态融合节点。我们针对始终正确的结构给出了否定答案。对于 n^8 <= U，log_2 U >= 2^70，以及冗余度 0 <= R < n，一个动态字典每次操作至少需要 2^-26 log_2(1+n/(R+1)) 的期望摊销单元探针。该模型允许每个至多一个字的打包单元的固定布局，包括简洁字 RAM 结构使用的短溢出约定，并涵盖具有每次调用全新随机性和几乎必然终止的零错误拉斯维加斯算法。证明通过将逐点探针上限置于一致性事件内部，修复了继承通信论证中的条件缺陷，然后通过尺度自适应熵参数将下界扩展到大型宇宙。因此，当 U=2^w 且 n=ceil(w^c)（对于任意固定 c>0）时，没有任何始终正确的前驱结构可以使用 log_2 binom(U,n)+o(n) 个持久可变位并支持常数时间操作。常数期望摊销时间需要 Omega(n) 个冗余位。Lean 4 检查了完整的打包内存和全新随机索引模型、硬分布、通信界限、分隔符、嵌套森林核算、确定性和拉斯维加斯下界、严格前驱归约以及冗余推论。
英文摘要
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.
Comments18 pages. The complete theorem chain and strict-predecessor consequence are checked in Lean 4. A companion reproducibility archive contains the exact formal sources, declaration map, axiom audit, manuscript source, and replay script. Reproducibility record: https://doi.org/10.5281/zenodo.22060084
