BCR Lemma 15: regrouping with an additive one-chunk loss

Disproved

KServer.bcr_lemma15_regroup

by kyle · Sep 6, 2026 · Mathlib c5ea003 (Lean v4.30.0)

k-serverlower-boundsprobability

Let $X$ be a metric space with marked points $s,t$ , let $\beta\ge2$ be an integer, and let $q>0$ and $R\ge0$ . Suppose a finite filtered chunk system from $s$ to $t$ has constant initial history, sizes in $[0,3q/2]$ , escape price $2\beta q$ , and expected total at least

3qR+3q.

Then there exists a chunk system on the same space and marked endpoints with constant initial history, sizes in $[3q/2,9q/2]$ , escape price $6\beta q$ , expected total at least $3qR$ , and at least $\lceil R\rceil$ chunks.

This is Lemma 15 specialized to average size $3q$ and maximum subchunk size $3q/2$ , with its escape-price conclusion. The surplus $3q$ covers the permitted loss in total and supplies the stated count lower bound. The restriction $\beta\ge2$ ensures

2\beta q+3q+\tfrac32q\le6\beta q.

The statement retains the existing offline bound and terminal singleton request through the chunk-system type. It is independent of the recursive BCR spaces and can be reused for other filtered request constructions.

Preamble

import Definitions.Def_KServer_bcr_induction

Formal statement

theorem KServer.bcr_lemma15_regroup {X : Type*} [MetricSpace X] {s t : X}
    (β : ℕ) (hβ : 2 ≤ β) (q R : ℝ) (hq : 0 < q) (hR : 0 ≤ R)
    (C : KServer.ChunkSystemB X s t 0 (3 * q / 2)
      (R * (3 * q) + 3 * q) (2 * β * q) 0)
    (h0 : ∀ ω₁ ω₂ : C.Ω, C.hist 0 ω₁ = C.hist 0 ω₂) :
    ∃ C' : KServer.ChunkSystemB X s t (3 * q / 2) (3 * (3 * q) / 2)
      (R * (3 * q)) (2 * β * (3 * q)) ⌈R⌉₊,
      ∀ ω₁ ω₂ : C'.Ω, C'.hist 0 ω₁ = C'.hist 0 ω₂ := by sorry

Source

Bubeck, Coester and Rabani, The Randomized k-Server Conjecture Is False!, arXiv:2211.05753v2, Section 4. https://arxiv.org/html/2211.05753v2, Lemma 15 and its application completing Lemma 12. Printed pp. 19–21.

View graph