BCR Claim 13: uniform subchunk induction step

Open

KServer.bcr_claim13_uniform

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

k-serverlower-boundsprobability

There exist constants $0<\alpha\le1$ and an integer $\beta\ge2$ , chosen independently of the level, such that for every $w\in\mathbb N$ with $\alpha(w+1)^2>1$ ,

\mathrm{BCRInductiveChunks}(\alpha,\beta,w)\ \Longrightarrow\ \mathrm{BCRInductiveSubchunks}(\alpha,\beta,w).

The input has sizes in $[3^w/2,3\cdot3^w/2]$ , escape price $2\beta3^w$ , at least $\lceil\alpha\beta w^2\rceil$ chunks and expected total at least $\alpha\beta w^2 3^w$ . The output is on the six-copy next-level space, with sizes in $[0,3\cdot3^w/2]$ , the same escape price, constant initial history, and expected total at least

\alpha\beta(w+1)^2 3^{w+1}+3\cdot3^w.

This is Claim 13 together with the uniform choice of constants in Section 4.2. It isolates the probabilistic construction and its cost analysis from regrouping and induction. No construction at all levels is assumed. Formalization note. All costs are multiplied by $3^w$ relative to the paper's normalization $d_w(s_w,t_w)=\beta$ .

Preamble

import Definitions.Def_KServer_bcr_induction

Formal statement

theorem KServer.bcr_claim13_uniform :
    ∃ α : ℝ, 0 < α ∧ α ≤ 1 ∧ ∃ β : ℕ, ∃ hβ : 0 < β,
      2 ≤ β ∧ ∀ w : ℕ, 1 < α * ((w + 1 : ℕ) : ℝ) ^ 2 →
        KServer.BCRInductiveChunks α β hβ w →
        KServer.BCRInductiveSubchunks α β hβ w := 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, Claim 13 and Sections 4.1–4.2, equations (1)–(5). Printed pp. 15–19.

View graph