← All papers
First page of Residual-Entropy Accounting for Routed Atom-Budgeted Learned Indexes

Residual-Entropy Accounting for Routed Atom-Budgeted Learned Indexes

Faruk Alpay, Levent Sarioglu

cs.DS May 27, 2026 · v1 cs.DB
A Lean 4 artifact, alongside Coq, machine-checks finite transcript, window and accounting invariants underlying the residual-entropy accounting theorem for learned indexes.
We study exact predecessor and rank search in a routed, atom-budgeted, certified-repair learned-index architecture. An ordered directory routes each query to a contiguous interval, a counted local predictor returns a certified rank window, and exact repair resolves the remaining uncertainty by comparisons. The result is scoped to this architecture and does not claim guarantees for arbitrary learned-index designs such as unconstrained RMI dispatch, hash routing, neural routing, or exact-payload indexes without additional accounting. The main parameter is conditional residual answer entropy: the entropy of the exact answer after the leaf, predictor output, certificate, and charged pre-repair information are observed. We prove a two-sided accounting theorem showing that this functional gives the query-time scale under the stated architecture and local predictor-atom budget. Directory space, sorted-array storage, and transcript-indexed repair-program space are treated as separate system costs, so the theorem is not a byte-level space lower bound or a compact implementation recipe. We also give a rank-spread specialization in which the radius term log(1 + Delta) is valid only when many residual ranks remain likely after the predictor transcript is known. For counted piecewise-linear segments, we make the profile term non-oracular, derive a shadow-price allocation rule, compute finite-instance RGapM and GapM values on real SOSD and Zenodo samples, and report benchmarks against PGM-index, RadixSpline, and binary search. The benchmarks expose overheads and bottlenecks rather than claiming speed for the shadow prototype.

The work seeks a single parameter for the query-time cost of exact predecessor and rank search in routed, atom-budgeted, certified-repair learned indexes. That parameter must couple routing entropy, approximation difficulty of the rank curve, and workload mass.

The authors define conditional residual answer entropy: the entropy of the exact answer after the leaf, predictor output, certificate, and charged pre-repair information are known. They prove a two-sided accounting theorem under a local predictor-atom budget and give a rank-spread radius specialization. They also derive a Lagrangian shadow-price allocation rule and closed forms under discrete power-law profiles. Modest Lean 4 and Coq files machine-check finite-interface invariants, such as residual offsets recovering window positions, singleton windows having zero ambiguity, and repair answers staying inside the transcript window.

The residual-entropy functional gives the query-time scale within the stated architecture. Exact finite RGapM and GapM values are computed on real SOSD and Zenodo samples. Benchmarks against PGM-index, RadixSpline and binary search show the overheads and bottlenecks of the diagnostic shadow prototype rather than speedups.