Prove2Me
Navigate
DiscoverFormalpediaBlogsUsersMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Deterministic kkk-server: no algorithm is ccc-competitive for c<kc<kc<k on the uniform space with k+1k+1k+1 points

Proved
KServer.uniform_not_competitive_below_k

by Gabewhigham · Sep 9, 2026 · Mathlib c5ea003 (Lean v4.30.0)

competitive-analysisk-serveronline-algorithms

The competitive ratio of deterministic kkk-server algorithms is at least kkk.

Let k≥1k \ge 1k≥1 and let MMM be the uniform metric space on k+1k+1k+1 points: MMM has exactly k+1k+1k+1 elements (witnessed by a bijection e:{0,…,k}→Me : \{0,\dots,k\} \to Me:{0,…,k}→M) and any two distinct points of MMM are at distance 111. This is the paging metric space with kkk pages of cache and k+1k+1k+1 distinct pages.

Then no deterministic online kkk-server algorithm on MMM is ccc-competitive for any c<kc < kc<k: for every algorithm AAA and every additive constant aaa there is a request sequence σ\sigmaσ with

costA(σ)>c⋅OPT(σ)+a.\mathrm{cost}_A(\sigma) > c \cdot \mathrm{OPT}(\sigma) + a .costA​(σ)>c⋅OPT(σ)+a.

This is the classical lower bound of Manasse, McGeoch and Sleator: the adversary always requests the unique point not covered by the algorithm, so the algorithm pays 111 per request, while an offline schedule that serves the requests in blocks of kkk consecutive requests pays at most n/k+kn/k + kn/k+k in total. It shows that the constant kkk in the kkk-server conjecture is the smallest possible, so the conjecture — if true — is tight.

Preamble
import Definitions.Def_KServer_model
Formal statement
namespace KServer

theorem uniform_not_competitive_below_k (k : ℕ) (hk : 1 ≤ k) (M : Type) [MetricSpace M]
    (e : Fin (k + 1) ≃ M) (hd : ∀ x y : M, x ≠ y → dist x y = 1)
    (A : OnlineAlgorithm k M) (c : ℝ) (hc : c < k) :
    ¬ IsCompetitive A c := by sorry

end KServer
Source
M. S. Manasse, L. A. McGeoch, D. D. Sleator, Competitive algorithms for server problems, Journal of Algorithms 11 (1990) 208-230, Theorem 1 (lower bound k for any metric space with at least k+1 points).

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