Lemma 9 (explicit form proved on p. 345) — ply three ≤ 4n/lg n, ply two ≤ 4n/lg⁽²⁾ n, ply-one components ≤ lg⁽²⁾ n

Proved

HarelTarjan.Compressed.lemma9_plies

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 \ge 4$ vertices, $C$ its compressed tree, and divide $C$ into plies one, two and three by rank, with thresholds $\lfloor \lg^{(3)} n\rfloor$ and $\lfloor \lg^{(2)} n \rfloor$ . Then:

Ply three contains at most $4n/\lg n$ vertices:

|\text{ply three}| \le \frac{4n}{\lg n}.

Ply two contains at most $4n/\lg^{(2)} n$ vertices:

|\text{ply two}| \le \frac{4n}{\lg^{(2)} n}.

Each connected component of ply one is a subtree of $C$ containing at most $\lg^{(2)} n$ vertices. Precisely: for every vertex $v$ in ply one, all descendants of $v$ in $C$ lie in ply one, and

\mathrm{size}_C(v) \le \lg^{(2)} n .

The paper states Lemma 9 with $O(n/\log n)$ and $O(n/\log^{(2)} n)$ ; its proof on p. 345 establishes the explicit constants $4$ and $4$ given here. The lemma is what makes the depth problem on $C$ solvable with linear preprocessing: the tables for plies two and three have total size $O(n)$ , and ply one splits into tiny subtrees.

Formalization Note $\lg$ is Real.logb 2, $n$ is Fintype.card V, and the plies use the iterated Nat.log thresholds of the definition Plies (equal to the real floors for $n \ge 4$ ). The hypothesis $n \ge 4$ is added: it is not on the page, where the $O(\cdot)$ hides it, and it makes $\lg n \ge 2$ and $\lg^{(2)} n \ge 1$ , so that the divisions are honest (Lean's $x/0 = 0$ ) and $\lg^{(3)} n \ge 0$ . Part 3 is the vertex-wise reading of "each connected component of ply one is a subtree of $C$ with at most $\lg^{(2)} n$ vertices": since ply one is closed under taking $C$ -descendants, the component of a ply-one vertex is the $C$ -subtree of its shallowest ply-one ancestor, and that subtree's size is bounded because its root lies in ply one.

Preamble

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

Formal statement

namespace HarelTarjan.Compressed

theorem lemma9_plies {V : Type*} [Fintype V] [DecidableEq V] (T : RootedTree V)
    (hn : 4 ≤ Fintype.card V) :
    ((ply3 T).card : ℝ) ≤ 4 * (Fintype.card V : ℝ) / Real.logb 2 (Fintype.card V) ∧
    ((ply2 T).card : ℝ) ≤
      4 * (Fintype.card V : ℝ) / Real.logb 2 (Real.logb 2 (Fintype.card V)) ∧
    ∀ v ∈ ply1 T,
      (∀ u : V, IsAncestorC T v u → u ∈ ply1 T) ∧
      (sizeC T v : ℝ) ≤ Real.logb 2 (Real.logb 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, Lemma 9 and its proof

Read-back

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

Fix a finite type $V$ with decidable equality, and write $n = |V|$ for its number of elements. Let $T$ be any value of type RootedTree V, a structure from the imported bundle HarelTarjan.Compressed. Its definition is not included in the code under audit. The only hypothesis is

n \ge 4 .

The statement uses four more objects from the imported bundle, and their definitions are not given here either. They are used only as follows:

$\mathrm{ply}_1(T)$ , $\mathrm{ply}_2(T)$ and $\mathrm{ply}_3(T)$ are finite collections, since each one has a cardinality and supports membership. The statement treats $\mathrm{ply}_1(T)$ as a collection of elements of $V$ .
$\mathrm{IsAncestorC}_T(v,u)$ is a relation between two elements $v, u$ of $V$ . The code does not say which direction counts as "ancestor".
$\mathrm{sizeC}_T(v)$ is a quantity attached to each $v \in V$ , converted to a real number for the comparison.

Nothing in the statement says what these objects are. In particular it does not say that the three plies are disjoint or that together they cover $V$ . Every property below is a property of whatever these definitions compute.

The theorem claims that all three of the following hold together, with $\log_2$ the real base-2 logarithm:

The third ply is small:

|\mathrm{ply}_3(T)| \;\le\; \frac{4n}{\log_2 n}.

The second ply is small:

|\mathrm{ply}_2(T)| \;\le\; \frac{4n}{\log_2 \log_2 n}.

The first ply has two properties. For every $v \in \mathrm{ply}_1(T)$ $v \in ply_{1} (T)$ :
- (a) every $u \in V$ with $\mathrm{IsAncestorC}_T(v,u)$ is also in $\mathrm{ply}_1(T)$ , so the first ply is closed under that relation, in the argument order written; and
- (b) the size is bounded:

\mathrm{sizeC}_T(v) \;\le\; \log_2 \log_2 n .

The three parts are joined by "and". Each bound uses the constant 4, and the inequalities are non-strict ( $\le$ ).

Degenerate cases. The hypothesis $n \ge 4$ rules out an empty or one-element $V$ . It also means $\log_2 n \ge 2$ and $\log_2 \log_2 n \ge 1$ . So both denominators are strictly positive, no division by zero happens, and no logarithm is taken of a non-positive number. Every bound is therefore a real, positive number, not a default value. At the smallest allowed size, $n = 4$ :

the bound on $|\mathrm{ply}_3(T)|$ is $16/2 = 8$ ;
the bound on $|\mathrm{ply}_2(T)|$ is $16/1 = 16$ ;
the bound on $\mathrm{sizeC}_T(v)$ for $v \in \mathrm{ply}_1(T)$ is $1$ .

If $\mathrm{ply}_1(T)$ is empty, part 3 holds trivially. Whether any of the conclusions is trivial for other reasons, for example because a ply is always empty or $\mathrm{sizeC}$ is always $0$ , depends on the imported definitions, which the code under audit does not show.

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