Lemma 5 — $\mathrm{size}_C(v) = \mathrm{size}_T(v)$ at an apex, and $\mathrm{size}_C(v) = 1$ otherwise

Proved

HarelTarjan.Compressed.lemma5_sizeC

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 and $C$ its compressed tree. For every vertex $v$ :

\mathrm{size}_C(v) = \begin{cases} \mathrm{size}_T(v) & \text{if } v \text{ is an apex},\\ 1 & \text{if } v \text{ is not an apex.}\end{cases}

So compression keeps the subtree of every apex intact (all its $T$ -descendants become its $C$ -descendants), while a vertex strictly inside a heavy path becomes a leaf of $C$ . This is the first structural fact about $C$ and leads to the size doubling of Lemma 6.

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 lemma5_sizeC {V : Type*} [Fintype V] [DecidableEq V] (T : RootedTree V) (v : V) :
    (IsApex T v → sizeC T v = size T v) ∧ (¬ IsApex T v → sizeC T v = 1) := by sorry

end HarelTarjan.Compressed

Source

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

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.

Definitions used.

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

Statement. The theorem asserts both of the following:

if $v$ is an apex, then $\operatorname{size}_C(v) = \operatorname{size}_T(v)$ ;
if $v$ is not an apex, then $\operatorname{size}_C(v) = 1$ .

Degenerate cases. The root is never heavy, so it is always an apex, and the first clause gives $\operatorname{size}_C(r) = \operatorname{size}_T(r) = |V|$ . If $V$ has one element, both sides equal $1$ . No hypothesis beyond the tree structure is involved, so the statement is not vacuous for any tree.

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 5 — sizeC(v)=sizeT(v)\mathrm{size}_C(v) = \mathrm{size}_T(v)sizeC​(v)=sizeT​(v) at an apex, and sizeC(v)=1\mathrm{size}_C(v) = 1sizeC​(v)=1 otherwise

Lemma 5 — $\mathrm{size}_C(v) = \mathrm{size}_T(v)$ at an apex, and $\mathrm{size}_C(v) = 1$ otherwise