Telescoping reduction: a potential with step bound yields sharp growth majorants

Disproved

KServer.growth_of_potential_coalesced

by jackjburleson · Sep 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

finite-reductionk-serverwork-function

Let $k\ge 1$ and let $M$ be any metric space with all servers starting at the point $p$ . Suppose a potential $\Phi$ on request prefixes satisfies, for some constant $C$ :

$\Phi(\sigma) \le (k+1)\,\mathrm{OPT}(p^k,\sigma) + C$ for every finite request sequence $\sigma$ ;
for every prefix $l$ , request $r$ , and injective configuration $Y$ ,

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

$\Phi([]) \le 0$ .

Then for every request sequence $\tau$ there exist simultaneous majorants $u_t$ of all unordered work-function increments at injective terminal configurations,

\widehat w_{p^k}(\tau_{\le t+1})(Y) \le \widehat w_{p^k}(\tau_{\le t})(Y) + u_t,

whose total mass is bounded:

\sum_{t<|\tau|} u_t \le (k+1)\,\mathrm{OPT}(p^k,\tau) + C.

This is a pure telescoping argument: take $u_t = \Phi(\tau_{\le t+1}) - \Phi(\tau_{\le t})$ , use the step bound with the identity $\tau_{\le t+1} = \tau_{\le t} \,\!+\!\!+[\tau_{t+1}]$ , and telescope the sum, which then collapses to $\Phi(\tau) - \Phi([])$ and is bounded by the upper bound at $\sigma = \tau$ . It is the reduction glue connecting KServer.potential_coalesced_k_ge3_finite to the sharp coalesced growth bound KServer.workFnU_growth_sharp_coalesced_finite (with $C = c$ from that theorem).

Preamble

import Definitions.Def_KServer_workfunctionU
open KServer

Formal statement

theorem KServer.growth_of_potential_coalesced
    (k : ℕ) (M : Type) [MetricSpace M]
    (p : M) (C : ℝ) (Φ : List M → ℝ)
    (hupper : ∀ σ : List M, Φ σ ≤ ((k : ℝ) + 1) * offlineCost (fun _ : Fin k => p) σ + C)
    (hstep : ∀ (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)
    (hnil : Φ [] ≤ 0)
    (τ : List M) :
    ∃ u : ℕ → ℝ,
      (∀ t, t < τ.length → ∀ Y : Config k M, Function.Injective Y →
        workFnU (fun _ => p) (τ.take (t + 1)) Y ≤
          workFnU (fun _ => p) (τ.take t) Y + u t) ∧
      (∑ t ∈ Finset.range τ.length, u t) ≤
        ((k : ℝ) + 1) * offlineCost (fun _ : Fin k => p) τ + C := by sorry

Source

Standard potential-function telescoping; cf. E. Koutsoupias, The k-server problem (2009), Section 3.4, https://users.cs.fiu.edu/~giri/teach/6936/S10/K-Server_CSReviews_09.pdf.

View graph