Proof of Theorem 1 (p. 340) — a nonleaf $w$ lies in $A_x$ for all leaves below one of its children

Proved

HarelTarjan.PointerLB.nonleaf_dichotomy

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

lower-boundnearest-common-ancestorp2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1pointer-machine

Let $T$ be the complete binary tree of height $h$ , represented in a list structure with two pointers per node by a map $\mathrm{rep}$ from vertices to nodes, and suppose that every nca query on two leaves is answered in $k$ steps. For a leaf $x$ let $A_x$ be the set of tree vertices whose nodes are accessible from $\mathrm{rep}(x)$ in $k$ steps or less.

Let $w$ be a nonleaf vertex of $T$ , with children $u = w0$ and $v = w1$ . Then either

w \in A_x \text{ for every leaf } x \text{ that is a descendant of } u, \quad\text{or}\quad w \in A_y \text{ for every leaf } y \text{ that is a descendant of } v.

This dichotomy is what forces every vertex to be seen from many leaves, and it drives the counting in the proof of Theorem 1.

Formalization Note The statement does not assume that $\mathrm{rep}$ is injective; the paper's representation is, and the claim holds without it.

Preamble

import Mathlib
import Definitions.Def_HarelTarjan_PointerLB_BinaryTree
import Definitions.Def_HarelTarjan_PointerLB_PointerMachine

Formal statement

namespace HarelTarjan.PointerLB

theorem nonleaf_dichotomy {N : Type*} {h k : ℕ} (ptr : N → Fin 2 → Option N)
    (rep : Vertex h → N) (hk : AnswersLeafQueriesIn ptr rep k)
    (w : Vertex h) (hw : w.1.length < h) :
    (∀ x : Vertex h, IsLeaf x → w.1 ++ [false] <+: x.1 → w ∈ A ptr rep k x) ∨
      (∀ y : Vertex h, IsLeaf y → w.1 ++ [true] <+: y.1 → w ∈ A ptr rep k y) := 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 ("We claim that either …")

Read-back

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

Setup.

$h,k\in\mathbb{N}$ , and $N$ is any type of nodes.
$\mathrm{ptr}$ assigns to each node $m$ and field $i\in\{0,1\}$ a node or nil.
$\mathrm{rep}$ is an arbitrary map, not necessarily injective, from vertices of the height- $h$ complete binary tree to nodes. A vertex is a boolean sequence of length at most $h$ ; a leaf is a vertex of length exactly $h$ .

Let $\mathrm{acc}_k(a)$ be the set of nodes reachable from $a$ by following at most $k$ non-nil pointer fields. For a vertex $x$ , define:

A_x=\{t : \mathrm{rep}(t)\in\mathrm{acc}_k(\mathrm{rep}(x))\}.

Hypotheses.

For every pair of leaves $x, y$ , some run of at most $k$ steps holds $\mathrm{rep}(\mathrm{nca}(x,y))$ . A run starts holding $[\mathrm{rep}(x),\mathrm{rep}(y)]$ , and each step adds a non-nil field $\mathrm{ptr}(m,i)$ of a held node $m$ . Here $\mathrm{nca}(x,y)$ is the longest common prefix of $x$ and $y$ .
$w$ is a vertex with $|w|<h$ , that is, a non-leaf.

Conclusion. At least one of the following holds:

for every leaf $x$ whose sequence begins with $w$ followed by false: $w\in A_x$ ;
for every leaf $y$ whose sequence begins with $w$ followed by true: $w\in A_y$ .

Degenerate cases.

When $h=0$ , no vertex satisfies $|w|<0$ , so the statement is vacuous.
If $\mathrm{rep}$ is not injective, " $w\in A_x$ " means only that the node $\mathrm{rep}(w)$ is reachable. That node may also represent other vertices.
For $k=0$ and $h\ge1$ , the query hypothesis can be satisfied only if $\mathrm{rep}(\mathrm{nca}(x,y))\in\{\mathrm{rep}(x),\mathrm{rep}(y)\}$ for all leaf pairs. This requires a non-injective $\mathrm{rep}$ ; otherwise the hypothesis is unsatisfiable.

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 nonleaf www lies in AxA_xAx​ for all leaves below one of its children

Proof of Theorem 1 (p. 340) — a nonleaf $w$ lies in $A_x$ for all leaves below one of its children