Proof of Lemma 9, p. 345 — at most $n/2^{k-1}$ vertices have rank $k$ or greater

Proved

HarelTarjan.Compressed.rank_ge_count

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

heavy-pathnearest-common-ancestorp2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1trees

Let $T$ be a rooted tree on $n$ vertices and $C$ its compressed tree. For every $k \ge 0$ , the number of vertices with rank $k$ or greater satisfies

\#\{\, v : \mathrm{rank}(v) \ge k \,\} \le \sum_{i=k}^{\infty} \frac{n}{2^i} = \frac{n}{2^{k-1}}.

This is the first sentence of the proof of Lemma 9 and yields the sizes of plies two and three.

Formalization Note The bound is stated without division as $\#\{v : \mathrm{rank}(v) \ge k\}\cdot 2^k \le 2n$ , which is $n/2^{k-1}$ over the reals, including $k = 0$ .

Preamble

import Mathlib
import Definitions.Def_HarelTarjan_Compressed_RootedTree
import Definitions.Def_HarelTarjan_Compressed_HeavyPath
import Definitions.Def_HarelTarjan_Compressed_CompressedTree

Formal statement

namespace HarelTarjan.Compressed

theorem rank_ge_count {V : Type*} [Fintype V] [DecidableEq V] (T : RootedTree V) (k : ℕ) :
    (Finset.univ.filter (fun v => k ≤ rank T v)).card * 2 ^ k ≤ 2 * Fintype.card V := by sorry

end HarelTarjan.Compressed

Source

Harel, Tarjan, Fast Algorithms for Finding Nearest Common Ancestors, SIAM J. Comput. 13 (1984), p. 345, proof of Lemma 9, first sentence

Read-back

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

Setting. $V$ is any finite type with decidable equality. $T$ is any rooted tree on $V$ with root $r$ and parent map $p$ , where:

$p(r) = r$ ;
every vertex reaches $r$ under some iterate $p^i$ , $i \ge 0$ .

$k$ is any natural number.

Definitions used.

$\operatorname{size}_T(w)$ is the number of $u$ with $p^j(u) = w$ for some $j \ge 0$ , including $w$ itself.
A vertex $x$ is heavy when $x \ne r$ and $\operatorname{size}_T(p(x)) < 2\,\operatorname{size}_T(x)$ .
$\operatorname{apex}(x) = p^m(x)$ for the least $m \ge 0$ with $p^m(x)$ not heavy.
The compressed parent is $p_C(r) = r$ , and $p_C(x) = \operatorname{apex}(p(x))$ for $x \ne r$ .
$\operatorname{size}_C(w)$ is the number of $u$ with $p_C^j(u) = w$ for some $j \ge 0$ , including $w$ itself.
$\operatorname{rank}(v) = \lfloor \log_2 \operatorname{size}_C(v) \rfloor$ .

Statement. The theorem asserts

\#\{v \in V : \operatorname{rank}(v) \ge k\} \cdot 2^k \le 2\,|V|.

In words: at most $2|V|/2^k$ vertices have rank at least $k$ .

Degenerate cases.

For $k = 0$ every vertex qualifies, and the claim is $|V| \le 2|V|$ , which is trivially true.
For $k$ exceeding every attained rank, the left side is $0$ .
If $|V| = 1$ , the claim is $1 \le 2$ for $k = 0$ and $0 \le 2$ otherwise.

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 Lemma 9, p. 345 — at most n/2k−1n/2^{k-1}n/2k−1 vertices have rank kkk or greater

Proof of Lemma 9, p. 345 — at most $n/2^{k-1}$ vertices have rank $k$ or greater