Lemma 8 — for any rank $i$ , the number of vertices of rank $i$ is at most $n/2^i$

Proved

HarelTarjan.Compressed.lemma8_rank_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, with $\mathrm{rank}(v) = \lfloor \lg \mathrm{size}_C(v)\rfloor$ . For every $i \ge 0$ ,

\#\{\, v : \mathrm{rank}(v) = i \,\} \le \frac{n}{2^i}.

Few vertices have high rank. Summed over $i \ge k$ this gives the count of high-rank vertices used for Lemma 9.

Formalization Note The bound is stated without division as $\#\{v : \mathrm{rank}(v) = i\}\cdot 2^i \le n$ , which is equivalent over the reals.

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 lemma8_rank_count {V : Type*} [Fintype V] [DecidableEq V] (T : RootedTree V) (i : ℕ) :
    (Finset.univ.filter (fun v => rank T v = i)).card * 2 ^ i ≤ Fintype.card V := by sorry

end HarelTarjan.Compressed

Source

Harel, Tarjan, Fast Algorithms for Finding Nearest Common Ancestors, SIAM J. Comput. 13 (1984), p. 344, Lemma 8

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$ .

$i$ 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^k(x)$ for the least $k \ge 0$ with $p^k(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) = i\} \cdot 2^i \le |V|.

In words: at most $|V|/2^i$ vertices have rank exactly $i$ .

Degenerate cases.

For $i = 0$ the claim is only that the number of rank- $0$ vertices is at most $|V|$ , which is trivially true.
For $i$ larger than every attained rank, the left side is $0$ .
If $|V| = 1$ , the single vertex has rank $0$ , and the claim reduces to $1 \le 1$ for $i = 0$ and $0 \le 1$ 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

Lemma 8 — for any rank iii, the number of vertices of rank iii is at most n/2in/2^in/2i

Lemma 8 — for any rank $i$ , the number of vertices of rank $i$ is at most $n/2^i$