An Exact Rounds-versus-Queries Trade-off for Pointer Chasing, Machine-Checked in Lean 4

Abstract

A deterministic query algorithm with $d$ rounds submits $d$ batches of queries, each chosen from the answers to earlier batches. Canonne and Gur asked for general bounds on the cost of removing rounds. For $k$-step pointer chasing over $k$ tables of $m \geq 2$ entries we determine this cost exactly: for $1 \leq d \leq k$, the least worst-case number of queries with at most $d$ rounds is exactly $(k-d)m+d$, so every round removed costs exactly $m-1$ queries, which is what the naive merging of two consecutive rounds pays. The lower bound uses an adversary that answers every query with the queried index, except at the first unread cell of the chain. The model, the problem and the theorem are formalised in Lean 4 without Mathlib, with no sorry and only the axioms propext and Quot.sound; an exhaustive search confirms the formula for small parameters.