The base case: a chunk system with online escapes on the path

Proved

KServer.chunk_system_b_base

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

k-serverlower-boundsmetrical-service-systems

The base case of BCR's Lemma 6 in the final (online-escape) package: on the path of $\beta+1$ equally spaced points, whenever $\alpha w^2 \le 1$ there is a deterministic chunk system with online-escape conditional cost bounds: $m = \beta$ chunks of size $1$ , an initial pinning request $\{0\}$ , singleton requests $\{i\}$ , trivial filtration, unit weights. The online-escape bounds follow from the already-established offline-escape bounds pointwise (escapeCost_le_bailCost).

Same content as chunk_system_base / chunk_system_f_base, in the package consumed by the combining and subchunk steps.

Preamble

import Mathlib
import Definitions.Def_KServer_evader
import Definitions.Def_KServer_chunk_system
import Definitions.Def_KServer_evader_bail
import Definitions.Def_KServer_chunk_system_b

Formal statement

namespace KServer

theorem chunk_system_b_base (β : ℕ) (hβ : 1 ≤ β) (α : ℝ) (hα0 : 0 ≤ α) (w : ℕ)
    (hw : α * (w : ℝ) ^ 2 ≤ 1) :
    letI := pathMetric β
    dist (0 : Fin (β + 1)) (Fin.last β) = β ∧
    Nonempty (ChunkSystemB (Fin (β + 1)) 0 (Fin.last β)
      (1 / 2) (3 / 2) (α * (w : ℝ) ^ 2 * β) (2 * β) ⌈α * β * (w : ℝ) ^ 2⌉₊) := by sorry

end KServer

Source

S. Bubeck, C. Coester, Y. Rabani, 'The randomized k-server conjecture is false!', STOC 2023, Lemma 6 (base case).

View graph