Potential function with sharp $(k+1)$ bound, step bound, and $c \le \Phi([])$ (coalesced start, finite metric)

Open

KServer.potential_coalesced_k_ge3_finite_sharp

by jackjburleson · Sep 7, 2026 · Mathlib c5ea003 (Lean v4.30.0)

competitive-analysisfinite-metrick-serverwork-function

Let $k\ge 3$ , let $M$ be a finite metric space, and place all $k$ servers initially at the single point $p$ (coalesced start). Then there exists a potential function $\Phi$ on request prefixes and a constant $c$ with $c \le \Phi([])$ such that:

Upper bound: for every finite request sequence $\sigma$ , $\Phi(\sigma) \le (k+1)\,\mathrm{OPT}(p^k,\sigma) + c$ .
Step bound: for every prefix $l$ , request $r$ , and injective terminal configuration $Y$ ,

\widehat w_{p^k}(l\,\!+\!\!+[r])(Y) - \widehat w_{p^k}(l)(Y) \le \Phi(l\,\!+\!\!+[r]) - \Phi(l).

The condition $c \le \Phi([])$ (for instance $c = \Phi([]) = 0$ ) is exactly what the sharp telescoping reduction KServer.growth_of_potential_sharp needs to produce growth majorants with total mass $\le (k+1)\,\mathrm{OPT}$ and no additive constant, resolving KServer.workFnU_growth_sharp_coalesced_finite. It generalizes KServer.workFnU_sharp_potential_known_cases ( $k\le 2$ or $|M|\le k+2$ ) to the remaining open cases of the sharp coefficient in E. Koutsoupias, The k-server problem (2009), Section 3.4, and Emek--Fraigniaud--Korman--Rosen (2009), Section 3.

Preamble

import Definitions.Def_KServer_workfunctionU
open KServer

Formal statement

theorem KServer.potential_coalesced_k_ge3_finite_sharp
    (k : ℕ) (hk : 3 ≤ k) (M : Type) [MetricSpace M] [Fintype M]
    (p : M) :
    ∃ Φ : List M → ℝ, ∃ c : ℝ,
      (∀ σ : List M, Φ σ ≤ ((k : ℝ) + 1) * offlineCost (fun _ : Fin k => p) σ + c) ∧
      (∀ (l : List M) (r : M) (Y : Config k M), Function.Injective Y →
        workFnU (fun _ => p) (l ++ [r]) Y - workFnU (fun _ => p) l Y ≤
          Φ (l ++ [r]) - Φ l) ∧
      (c ≤ Φ []) := by sorry

Source

Proposed potential-form of the open sharp extended-cost criterion in E. Koutsoupias, The k-server problem (2009), Section 3.4, https://users.cs.fiu.edu/~giri/teach/6936/S10/K-Server_CSReviews_09.pdf, equation (6); cf. Emek--Fraigniaud--Korman--Rosen, https://arxiv.org/pdf/0902.1378.

View graph

Potential function with sharp (k+1)(k+1)(k+1) bound, step bound, and c≤Φ([])c \le \Phi([])c≤Φ([]) (coalesced start, finite metric)

Potential function with sharp $(k+1)$ bound, step bound, and $c \le \Phi([])$ (coalesced start, finite metric)