Canonne and Gur asked for general bounds on the cost of removing rounds of adaptivity from deterministic query algorithms. The paper studies this cost exactly for k-step pointer chasing over k tables of m entries.

Query strategies are modelled as trees that submit batches of cells per round, with depth and cost defined as predicates on the tree. The upper bound follows the chain one cell per round and reads the last k-d tables in full. The lower bound uses an adversary that answers each query with the queried index, except at the first unread chain cell. The model, the problem and both bounds are formalised in Lean 4.22.0 using only the core library, and an exhaustive search checks small parameters.

With 1 ≤ d ≤ k rounds the least worst-case number of queries is exactly (k−d)m+d, so each removed round costs exactly m−1 queries, the same as naively merging two rounds. The Lean proofs contain no sorry and depend only on the axioms propext and Quot.sound; a few parts, such as the distinct-cell form of the lower bound and the asymptotic corollary, are checked on paper only.