BCR Lemma 12 and Claim 13: quantitative induction packages

Definition

KServer_bcr_induction

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

The quantitative induction packages in BCR Lemma 12 and Claim 13, expressed at the canonical metric scale

d(s_w,t_w)=\beta 3^w.

BCRInductiveChunks requires chunk sizes in $[3^w/2,3\cdot3^w/2]$ , escape price $2\beta3^w$ , expected total at least $\alpha\beta w^2 3^w$ , and at least $\lceil\alpha\beta w^2\rceil$ chunks. The existing chunk-system structure records adaptation, conditional cost bounds, the final singleton request, and the offline upper bound. Initial history is constant.

BCRInductiveSubchunks records the intermediate construction on level $w+1$ : sizes in $[0,3\cdot3^w/2]$ , escape price $2\beta3^w$ , and expected total at least

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

The surplus pays for regrouping. These are predicates on concrete chunk systems, with no assumed existence results.

Definition code

import Definitions.Def_KServer_bcr_space2
import Definitions.Def_KServer_chunk_system_b

namespace KServer

/-- The seven quantitative conditions of BCR Lemma 12, at the unnormalized
scale `dist s t = β * 3 ^ w`, together with trivial initial information. -/
def BCRInductiveChunks (α : ℝ) (β : ℕ) (hβ : 0 < β) (w : ℕ) : Prop :=
  ∃ C : @ChunkSystemB (bcrLevel2 β hβ w).carrier (bcrLevel2 β hβ w).metric
      (bcrLevel2 β hβ w).s (bcrLevel2 β hβ w).t
      ((3 : ℝ) ^ w / 2) (3 * (3 : ℝ) ^ w / 2)
      ((α * β * (w : ℝ) ^ 2) * 3 ^ w) (2 * β * (3 : ℝ) ^ w)
      ⌈α * β * (w : ℝ) ^ 2⌉₊,
    ∀ ω₁ ω₂ : C.Ω, C.hist 0 ω₁ = C.hist 0 ω₂

/-- Claim 13 before regrouping: the next level has smaller subchunks and an
extra `3 * 3 ^ w` of expected cost to pay for the regrouping loss. -/
def BCRInductiveSubchunks (α : ℝ) (β : ℕ) (hβ : 0 < β) (w : ℕ) : Prop :=
  ∃ C : @ChunkSystemB (bcrLevel2 β hβ (w + 1)).carrier
      (bcrLevel2 β hβ (w + 1)).metric
      (bcrLevel2 β hβ (w + 1)).s (bcrLevel2 β hβ (w + 1)).t
      0 (3 * (3 : ℝ) ^ w / 2)
      ((α * β * ((w + 1 : ℕ) : ℝ) ^ 2) * 3 ^ (w + 1) + 3 * (3 : ℝ) ^ w)
      (2 * β * (3 : ℝ) ^ w) 0,
    ∀ ω₁ ω₂ : C.Ω, C.hist 0 ω₁ = C.hist 0 ω₂

end KServer

Source

Bubeck, Coester and Rabani, The Randomized k-Server Conjecture Is False!, arXiv:2211.05753v2, Section 4. https://arxiv.org/html/2211.05753v2, Lemma 12 and Claim 13.

View graph