Lemma 6 — every edge $v \to p_C(v)$ of $C$ satisfies $2\cdot\mathrm{size}_C(v) \le \mathrm{size}_C(p_C(v))$

Proved

HarelTarjan.Compressed.lemma6_sizeC_doubles

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 with root $r$ and $C$ its compressed tree. Every edge $v \to p_C(v)$ of $C$ , that is, every vertex $v \ne r$ , satisfies

2\cdot \mathrm{size}_C(v) \le \mathrm{size}_C(p_C(v)).

Sizes in $C$ at least double from child to parent. This is the fact behind the shallow depth of $C$ (Lemma 7) and the rank counting of Lemma 8.

Formalization Note The hypothesis $v \ne r$ expresses that $v \to p_C(v)$ is an edge of $C$ ; for the root, where the Lean map has $p_C(r) = r$ , the inequality would be false.

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 lemma6_sizeC_doubles {V : Type*} [Fintype V] [DecidableEq V] (T : RootedTree V) (v : V)
    (hv : v ≠ T.root) :
    2 * sizeC T v ≤ sizeC T (pC T v) := by sorry

end HarelTarjan.Compressed

Source

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

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

$v$ is any vertex with $v \ne r$ .

Definitions used.

$\operatorname{size}_T(w)$ is the number of $u$ with $p^i(u) = w$ for some $i \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^i(u) = w$ for some $i \ge 0$ , including $w$ itself.

Statement. The theorem asserts

2\,\operatorname{size}_C(v) \le \operatorname{size}_C\big(p_C(v)\big),

where $p_C(v) = \operatorname{apex}(p(v))$ because $v \ne r$ . The inequality is non-strict.

The statement applies to every non-root vertex. It is not restricted to apex vertices.

Degenerate cases. If $V$ has exactly one element, no vertex satisfies $v \ne r$ , so the statement is vacuously true. For the root itself nothing is asserted.

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 6 — every edge v→pC(v)v \to p_C(v)v→pC​(v) of CCC satisfies 2⋅sizeC(v)≤sizeC(pC(v))2\cdot\mathrm{size}_C(v) \le \mathrm{size}_C(p_C(v))2⋅sizeC​(v)≤sizeC​(pC​(v))

Lemma 6 — every edge $v \to p_C(v)$ of $C$ satisfies $2\cdot\mathrm{size}_C(v) \le \mathrm{size}_C(p_C(v))$