Prove2Me
Navigate
MissionsFormalpediaBlogsUsersMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Every k-server algorithm is dominated by a lazy simple one

Proved
KServer.exists_lazy_injective_algorithm

by Shuze Chen · Sep 1, 2026 · Mathlib c5ea003 (Lean v4.30.0)

k-serverlazinessmatchingonline-algorithms

Every deterministic online kkk-server algorithm whose initial configuration places the servers on kkk distinct points is dominated by one that is lazy and simple: starting from the same configuration and never paying more on any request sequence, the dominating algorithm keeps its servers on kkk distinct points at all times, moves nothing when a request is already covered, and otherwise moves exactly one server, directly onto the request.

Role

This strengthens the classical laziness reduction (exists_lazy_algorithm) by additionally maintaining injectivity of the configurations. On a space of k+1k+1k+1 points, a simple configuration leaves exactly one point uncovered — the hole — and a lazy simple algorithm moves precisely when the hole is requested, paying the distance the hole travels. This makes the kkk-server problem on k+1k+1k+1 points literally the evader problem (metrical service systems), which is the reduction underlying the Bubeck–Coester–Rabani Ω(log⁡2k)\Omega(\log^2 k)Ω(log2k) randomized lower bound.

Proof idea

The dominating algorithm simulates A\mathcal{A}A while maintaining the potential Φ=\Phi = Φ= the minimum-cost perfect matching between its configuration and A\mathcal{A}A's. On a covered request it stays (and Φ\PhiΦ grows by at most A\mathcal{A}A's step cost, since the matching cost is 111-Lipschitz). On an uncovered request rrr it moves the server matched to a server of A\mathcal{A}A standing on rrr; the move costs exactly the matched edge, which the new matching saves, so the step cost plus the new potential is at most the old potential plus A\mathcal{A}A's step cost. Telescoping with Φ0=0\Phi_0 = 0Φ0​=0 dominates the total cost. Injectivity is preserved because the moved server lands on a previously uncovered point.

Formalization note

Laziness is expressed by the last two conjuncts: no motion on covered requests, and a one-server update otherwise. The minimum-cost matching ranges over permutations of Fin k.

Preamble
import Mathlib
import Definitions.Def_KServer_model
Formal statement
namespace KServer

theorem exists_lazy_injective_algorithm (k : ℕ) (M : Type*) [MetricSpace M]
    (A : OnlineAlgorithm k M) (hinj : Function.Injective (A.conf [])) :
    ∃ B : OnlineAlgorithm k M,
      B.conf [] = A.conf [] ∧
      (∀ σ : List M, B.cost σ ≤ A.cost σ) ∧
      (∀ l : List M, Function.Injective (B.conf l)) ∧
      (∀ (l : List M) (r : M), (∃ i, B.conf l i = r) → B.conf (l ++ [r]) = B.conf l) ∧
      (∀ (l : List M) (r : M), ∃ i : Fin k, B.conf (l ++ [r]) = Function.update (B.conf l) i r) := by sorry

end KServer
Source
Classical (implicit in M. Manasse, L. McGeoch, D. Sleator 1990 and standard k-server surveys: configurations may be assumed simple and algorithms lazy); needed for the hole/evader reduction of S. Bubeck, C. Coester, Y. Rabani, STOC 2023.

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactJoin Slack© 2026 Prove2Me