Prove2Me

Anchored potential shift: Φx(ℓr)−Φx(ℓ)=w^ℓr(rˉk)−w^ℓ(rˉk)\Phi_x(\ell r)-\Phi_x(\ell)=\widehat w_{\ell r}(\bar r^k)-\widehat w_\ell(\bar r^k) for xk=rx_k=r

Proved
KServer.ckPotAtK_snoc_of_anchor_last

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

k-serveronline-algorithmswork-function

Let MM be a metric space, let Δ>0\Delta>0 bound all its distances, and let N=M⊔MˉN=M\sqcup\bar M be the antipodal extension of MM at scale Δ\Delta, in which every point qq has an antipode qˉ\bar q with d(y,q)+d(y,qˉ)=2Δd(y,q)+d(y,\bar q)=2\Delta. Fix k≥1k\ge 1 servers with initial configuration C0C_0 in MM, write w^τ\widehat w_\tau for the unordered work function of the instance evaluated in NN, and write

Φx(τ)  =  w^τ(x1⋯xk)  +  ∑i=1kw^τ(xˉi i xi+1⋯xk)\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)

for the anchored Coester--Koutsoupias potential of the anchor tuple x=(x1,…,xk)x=(x_1,\dots,x_k) (KServer.ckPotAtK).

Statement. For every request sequence ℓ\ell, every request r∈Mr\in M and every anchor tuple xx whose last coordinate is the request, xk=rx_k=r,

Φx(ℓr)−Φx(ℓ)  =  w^ℓr(rˉ k)−w^ℓ(rˉ k).\Phi_x(\ell r)-\Phi_x(\ell)\;=\;\widehat w_{\ell r}(\bar r^{\,k})-\widehat w_{\ell}(\bar r^{\,k}).

In words: serving rr shifts the anchored potential of every anchor tuple ending at rr by exactly the growth of the work function at the coalesced antipode of rr, which is the quantity appearing on the left of the Coester--Koutsoupias step inequality.

The reason is that among the k+1k+1 configurations occurring in Φx\Phi_x, all but the last contain the base point rr itself: the base configuration x1⋯xkx_1\cdots x_k has xk=rx_k=r, and for i<ki<k the configuration xˉi ixi+1⋯xk\bar x_i^{\,i}x_{i+1}\cdots x_k retains the coordinate xk=rx_k=r. A configuration that already occupies the requested point has an unchanged work function after that request, since the work function is monotone under appending a request and the optimal schedule may stop at that configuration. The remaining configuration, the one with index i=ki=k, is xˉk k=rˉ k\bar x_k^{\,k}=\bar r^{\,k}, whose value grows by the stated amount.

Formalization note. The last coordinate is the index ⟨k−1⟩\langle k-1\rangle of Fin k, whose bound follows from 1≤k1\le k; requests are carried into NN by List.map Sum.inl and the antipode of rr is Sum.inr r.

Preamble
import Mathlib
import Definitions.Def_KServer_ck_potential_k
Formal statement
namespace KServer

theorem ckPotAtK_snoc_of_anchor_last (k : ℕ) (hk : 1 ≤ k) (M : Type) [MetricSpace M]
    (Δ : ℝ) (hΔ0 : 0 < Δ) (hΔ : ∀ x y : M, dist x y ≤ Δ) (C₀ : Config k M)
    (l : List M) (r : M) (x : Fin k → M) (hx : x ⟨k - 1, by omega⟩ = r) :
    ckPotAtK k M Δ hΔ0 hΔ C₀ (l ++ [r]) x - ckPotAtK k M Δ hΔ0 hΔ C₀ l x
      = @workFnU k (M ⊕ M) (antipodalExtension M Δ hΔ0 hΔ) (fun i => Sum.inl (C₀ i))
          ((l ++ [r]).map Sum.inl) (fun _ => Sum.inr r)
        - @workFnU k (M ⊕ M) (antipodalExtension M Δ hΔ0 hΔ) (fun i => Sum.inl (C₀ i))
          (l.map Sum.inl) (fun _ => Sum.inr 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 (the potential Phi); the identity is the elementary observation underlying the role of the anchor property in the step inequality.

View graph