Prove2Me

Sharp work-function potentials for at most two servers or at most k+2 points

Proved
KServer.workFnU_sharp_potential_known_cases

by Wenqian · Sep 6, 2026 · Mathlib c5ea003 (Lean v4.30.0)

competitive-analysisk-serverwork-function

Fix k≥1k\ge1, a metric space MM, and an initial configuration C0C_0. Suppose either k≤2k\le2, or MM has at most k+2k+2 distinct points. Write w^l(X)\widehat w_l(X) for the unordered work function. There exist a real-valued history potential Φ\Phi and a real constant cc such that

Φ(l)≤(k+1) OPT(C0,l)+c,\Phi(l)\le(k+1)\,\mathrm{OPT}(C_0,l)+c, w^lr(X)−w^l(X)≤Φ(lr)−Φ(l)\widehat w_{lr}(X)-\widehat w_l(X)\le\Phi(lr)-\Phi(l)

for every finite history, next request, and injective configuration XX.

This packages the established sharp small cases in the common history-potential interface. The initial configuration may have repeated points, and the constant is fixed for all histories. When k≤2k\le2, the metric can be infinite or unbounded. This theorem does not assert the general sharp potential for larger server counts and larger metric spaces.

Formalization Note Having at most k+2k+2 points is expressed by the absence of an injective map from Fin (k + 3) to MM, so the statement needs no chosen enumeration of MM.

Preamble
import Definitions.Def_KServer_workfunctionU
open KServer
Formal statement
theorem KServer.workFnU_sharp_potential_known_cases (k : ℕ) (hk : 1 ≤ k) (M : Type) [MetricSpace M]
    (C₀ : Config k M)
    (hsmall : k ≤ 2 ∨ ¬ ∃ f : Fin (k + 3) → M, Function.Injective f) :
    ∃ Φ : List M → ℝ, ∃ c : ℝ,
      (∀ σ : List M, Φ σ ≤ ((k : ℝ) + 1) * offlineCost C₀ σ + c) ∧
      (∀ (l : List M) (r : M) (X : Config k M), Function.Injective X →
        workFnU C₀ (l ++ [r]) X - workFnU C₀ l X ≤ Φ (l ++ [r]) - Φ l) := by sorry
Source
History-potential consequences of the established small-case work-function growth results in E. Koutsoupias, The k-server problem (2009), https://users.cs.fiu.edu/~giri/teach/6936/S10/K-Server_CSReviews_09.pdf, Section 3.4, Lemma 2, equation (6), preprint p. 12; potential method pp. 13-15, including Theorems 2-3 and the k+1 and k+2 point cases. K. Brilliantov, E. Bamas, E. Abbe, k-server-bench, https://arxiv.org/html/2604.07240v1, Appendix B.1 Definition 2 and B.2 Theorem 1. The small-case growth theorems are reused from Shuze Chen's proved platform formalizations.

View graph