Prove2Me

The Coester--Koutsoupias potential is minimised at an anchor tuple ending in the request, for k≤2k \le 2

Proved
KServer.ckPotK_anchor_at_request_le_two

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

competitive-analysisk-serveronline-algorithmswork-function

Let MM be a finite metric space, let Δ>0\Delta>0 bound all of its distances, and let N=M⊔MˉN = M \sqcup \bar M be the antipodal extension of MM at scale Δ\Delta. Fix kk servers, an initial configuration C0C_0 in MM and a request sequence τ\tau, and write w^τ\widehat w_\tau for the unordered work function of that instance evaluated in NN. For an anchor tuple x=(x1,…,xk)∈Mkx = (x_1,\dots,x_k) \in M^k the anchored Coester--Koutsoupias potential and the potential itself are

Φx(τ)=w^τ(x1⋯xk)+∑i=1kw^τ(xˉi i xi+1⋯xk),Φ(τ)=min⁡x∈MkΦx(τ).\Phi_x(\tau) = \widehat w_\tau(x_1\cdots x_k) + \sum_{i=1}^{k}\widehat w_\tau\bigl(\bar x_i^{\,i}\,x_{i+1}\cdots x_k\bigr), \qquad \Phi(\tau) = \min_{x \in M^k}\Phi_x(\tau).

Statement. For k∈{1,2}k \in \{1,2\}, every request sequence ℓ\ell and every request r∈Mr \in M, the minimum defining Φ(ℓr)\Phi(\ell r) is attained at an anchor tuple whose last coordinate is the request: there is x∈Mkx \in M^k with xk=rx_k = r and Φx(ℓr)=Φ(ℓr)\Phi_x(\ell r) = \Phi(\ell r).

This is the anchor condition of Corollary 9 of Coester--Koutsoupias, in the two cases where it is unconditionally true. For one server the potential after the request does not depend on the anchor at all. For two servers the argument uses only two structural properties of the work function after a request: that it is 11-Lipschitz for the matching distance, and that it resolves the request, in the sense that

w^ℓr(a,b)=min⁡(h^(b)+d(a,ρ), h^(a)+d(b,ρ)),h^(z):=w^ℓr(ρ,z),\widehat w_{\ell r}(a,b) = \min\bigl(\widehat h(b) + d(a,\rho),\ \widehat h(a) + d(b,\rho)\bigr), \qquad \widehat h(z) := \widehat w_{\ell r}(\rho, z),

where ρ\rho is the request seen in the base copy. The whole potential is thus expressible through the single 11-Lipschitz function h^\widehat h, and the conclusion follows from a four-case comparison, each case using exactly one Lipschitz estimate.

For k≥3k \ge 3 these two properties no longer suffice, and the statement itself is in fact false in general: Section 7.2 of the same paper exhibits a request sequence on the circle with k=3k=3 for which the potential fails the corresponding step inequality. The present statement therefore delimits the range in which the anchor condition holds unconditionally.

Formalization note. The last coordinate is written x ⟨k - 1, _⟩ with 00-based indexing. The hypothesis hΔ asks only that Δ\Delta be an upper bound for the distances of MM, not that it be the diameter.

Preamble
import Mathlib
import Definitions.Def_KServer_workfunctionU
import Definitions.Def_KServer_antipodal_extension
import Definitions.Def_KServer_ck_potential_k
Formal statement
namespace KServer

theorem ckPotK_anchor_at_request_le_two (k : ℕ) (hk : 1 ≤ k) (hk2 : k ≤ 2) (M : Type)
    [MetricSpace M] [Fintype M] (Δ : ℝ) (hΔ0 : 0 < Δ) (hΔ : ∀ x y : M, dist x y ≤ Δ)
    (C₀ : Config k M) (l : List M) (r : M) :
    ∃ x : Fin k → M, x ⟨k - 1, by omega⟩ = r ∧
      ckPotAtK k M Δ hΔ0 hΔ C₀ (l ++ [r]) x = ckPotK k M Δ hΔ0 hΔ C₀ (l ++ [r]) := 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, Corollary 9 (printed p. 8), the cases k = 1 and k = 2 of its hypothesis; the failure for k = 3 is Section 7.2 of the same paper (printed pp. 22-23).

View graph