Proof of Theorem 1 (p. 340) — a query answered in $k$ steps reaches only nodes accessible in $k$ steps

Proved

HarelTarjan.PointerLB.answered_mem_acc

by mikedeng1 · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

lower-boundp2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1pointer-machine

Consider a list structure in which every node has two pointer fields. Let $a, b$ be the input nodes of a query and $c$ a node. If the query with answer $c$ can be answered in $k$ steps, that is, some run of at most $k$ pointer-following steps from $a, b$ holds a pointer to $c$ , then

c \in \mathrm{acc}_k(a) \cup \mathrm{acc}_k(b),

where $\mathrm{acc}_k(a)$ is the set of nodes accessible from $a$ in $k$ steps or less.

Contrapositively, a node accessible from neither input in $k$ steps cannot be returned in $k$ steps. This is the step from the machine to accessibility in the proof of Theorem 1: "w would be accessible from neither x nor y in k steps, and an nca query on x and y would be unanswerable in k steps."

Preamble

import Mathlib
import Definitions.Def_HarelTarjan_PointerLB_BinaryTree
import Definitions.Def_HarelTarjan_PointerLB_PointerMachine

Formal statement

namespace HarelTarjan.PointerLB

theorem answered_mem_acc {N : Type*} (ptr : N → Fin 2 → Option N) (a b target : N) (k : ℕ)
    (hans : AnsweredIn ptr a b target k) :
    target ∈ acc ptr k a ∪ acc ptr k b := by sorry

end HarelTarjan.PointerLB

Source

Harel, Tarjan, Fast Algorithms for Finding Nearest Common Ancestors, SIAM J. Comput. 13 (1984), p. 340, proof of Theorem 1, first paragraph, last sentence

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Let $N$ be any type of nodes. Let $\mathrm{ptr}$ be a pointer structure: it assigns to each node $m$ and field $i\in\{0,1\}$ either a node $\mathrm{ptr}(m,i)$ or nil. Let $a$ , $b$ and $\tau$ be nodes, and let $k\in\mathbb{N}$ .

The accessible sets are defined by:

\mathrm{acc}_0(a)=\{a\},\qquad \mathrm{acc}_{j+1}(a)=\mathrm{acc}_j(a)\cup\{n:\exists m\in\mathrm{acc}_j(a),\ \exists i,\ \mathrm{ptr}(m,i)=n\}.

A run works as follows:

It starts at step $0$ holding the list $[a,b]$ .
Each step picks a held node $m$ and a field $i$ with $\mathrm{ptr}(m,i)=n$ non-nil, and adds $n$ to the held list.

Hypothesis: some run of $t\le k$ steps holds $\tau$ .

Conclusion:

\tau\in\mathrm{acc}_k(a)\ \cup\ \mathrm{acc}_k(b).

Degenerate cases. With $k=0$ , the hypothesis means $\tau\in\{a,b\}$ , and the conclusion is the same statement. If $a=b$ , the conclusion is $\tau\in\mathrm{acc}_k(a)$ . No finiteness or other condition is placed on $N$ or $\mathrm{ptr}$ .

Human review

Endorsed by Shuze Chen · Sep 27, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Sep 27, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Proof of Theorem 1 (p. 340) — a query answered in kkk steps reaches only nodes accessible in kkk steps

Proof of Theorem 1 (p. 340) — a query answered in $k$ steps reaches only nodes accessible in $k$ steps