Prove2Me
Navigate
MissionsFormalpediaBlogsUsersMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

CK 2021, Theorem 23 — WFA is 333-competitive for 333 servers on trees

Proved
KServer.wfaU_trees_three_competitive

by Shuze Chen · Sep 1, 2026 · Mathlib c5ea003 (Lean v4.30.0)

competitive-analysisk-serveronline-algorithmstreeswork-function

Theorem 23 of Coester and Koutsoupias. The Work Function Algorithm is 333-competitive for 333 servers on trees.

Let MMM be the vertex set of a finite weighted tree, carrying the path metric, and let C0C_0C0​ be an initial configuration of three servers. Then there is a constant aaa, depending on the space and on C0C_0C0​ but not on the request sequence, with

cost(WFA,σ)  ≤  3⋅OPT(σ)+afor every σ.\mathrm{cost}(\mathrm{WFA}, \sigma) \;\le\; 3 \cdot \mathrm{OPT}(\sigma) + a \qquad \text{for every } \sigma.cost(WFA,σ)≤3⋅OPT(σ)+afor every σ.

Since kkk-competitiveness is conjectured to be optimal and is known to be a lower bound for every deterministic algorithm on any metric space with more than kkk points, this is a tight bound for k=3k = 3k=3: it settles the kkk-server conjecture for three servers on trees.

Context

The general upper bound for the Work Function Algorithm is 2k−12k-12k−1, which gives 555 for three servers. Bringing it down to kkk has been achieved only on restricted spaces --- the line, spaces of k+1k+1k+1 and k+2k+2k+2 points, the Manhattan plane for k=3k=3k=3 --- and trees for k=3k=3k=3 is the case Coester and Koutsoupias settle, by exhibiting a potential function satisfying an offset and an update property, the latter proved using the fact that a metric is a tree metric exactly when it is quasiconcave.

What WFA means here

The algorithm is the classical one: after each request it moves to a configuration containing the request minimising movement cost plus the work function of the unlabelled configuration --- the work function whose final move is a minimum-cost matching, which is the one all of the classical theory concerns.

The distinction matters. A configuration is formally a function {1,2,3}→M\{1,2,3\} \to M{1,2,3}→M, and one can build a work function that demands server iii finish at a named point; the resulting algorithm is a different one, and it is not 333-competitive on trees. On the path 0−1−2−30 - 1 - 2 - 30−1−2−3 with edge weights 2,4,42, 4, 42,4,4 and initial configuration (1,0,3)(1,0,3)(1,0,3) there is an admissible run of that variant which is eventually periodic with period 777, of cost 282828 per period against an optimal offline cost of 888, so its ratio tends to 7/27/27/2 and no additive constant suffices. The loss is a step whose labelled cost is 888 while the matching between the same two point sets costs 444: two servers exchange positions and buy nothing. Minimising against the unlabelled work function removes exactly this, because the work function is then blind to the labelling while the movement cost is not, so the minimisation itself selects the matching.

Formalization note

IsTreeVertexSpace M says the metric on MMM is the path metric of a weighted tree whose vertex set is MMM itself. WFAU is the classical Work Function Algorithm as above; ties in its step are broken by a fixed arbitrary choice, and the statement is asserted for that algorithm however they are broken. IsCompetitive A c is the usual ∃a,∀σ, cost≤c⋅OPT+a\exists a, \forall \sigma,\ \mathrm{cost} \le c \cdot \mathrm{OPT} + a∃a,∀σ, cost≤c⋅OPT+a, with OPT\mathrm{OPT}OPT the optimal offline cost from AAA's initial configuration.

Preamble
import Mathlib
import Definitions.Def_KServer_wfaU
import Definitions.Def_KServer_tree_metric
Formal statement
namespace KServer

theorem wfaU_trees_three_competitive {M : Type*} [MetricSpace M] [Fintype M]
    (hM : IsTreeVertexSpace M) (C₀ : Config 3 M) :
    IsCompetitive (WFAU (Nat.succ_pos 2) C₀) 3 := by sorry

end KServer
Source
C. Coester, E. Koutsoupias, 'Towards the k-server conjecture: a unifying potential, pushing the frontier to the circle', ICALP 2021, arXiv:2102.10474, Section on trees, Theorem 23: 'WFA is 3-competitive for 3 servers on trees.'

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactJoin Slack© 2026 Prove2Me