Always-Correct Succinct Dynamic Fusion Nodes Are Impossible: A Cell-Probe Lower Bound in the Small-Set, Large-Universe Regime

Abstract

This record contains the paper and reproducibility package for a cell-probe lower bound that rules out always-correct succinct constant-time dynamic fusion nodes in the fixed-layout packed-memory model. The package includes the full Lean 4 formalization for deterministic and fresh-random Las Vegas execution, a theorem-to-declaration map, an axiom audit, deterministic manifests, and manuscript build inputs.