Prove2Me

BCR 2023, Lemma 12 — chunk systems on the canonical BCR spaces bcrLevel2\mathrm{bcrLevel2}

Open
KServer.bcr_level_system

by doctosil · Sep 5, 2026 · Mathlib c5ea003 (Lean v4.30.0)

k-servermetric-spacesonline-algorithmsprobability

The BCR Lemma 12 chunk system existence on canonical Θ\Theta-glued spaces.

For the canonical recursive metric space family bcrLevel2 β hβ w of Bubeck--Coester--Rabani (STOC 2023), there exist positive constants α>0\alpha > 0 and β≥1\beta \ge 1 such that for every level w∈Nw \in \mathbb{N}, the space carrying diameter d(sw,tw)=β⋅3wd(s_w, t_w) = \beta \cdot 3^w supports a chunk system with size floor 00, nonnegative escape price, trivial initial history, and expected total size at least

Tw  ≥  α w2 (β⋅3w)  =  α w2 d(sw,tw).T_w \;\ge\; \alpha\, w^2\, (\beta \cdot 3^w) \;=\; \alpha\, w^2\, d(s_w, t_w).

This isolates the pure recursive chunk system construction from the ambient metric space embedding and cardinality bookkeeping.

Preamble
import Mathlib
import Definitions.Def_KServer_model
import Definitions.Def_KServer_evader
import Definitions.Def_KServer_evader_bail
import Definitions.Def_KServer_chunk_system_b
import Definitions.Def_KServer_bcr_space2
Formal statement
namespace KServer

theorem bcr_level_system :
    ∃ α : ℝ, 0 < α ∧ ∃ β : ℕ, ∃ hβ : 0 < β, ∀ w : ℕ,
      ∃ (cHi price : ℝ) (M : ℕ)
        (C : @ChunkSystemB (bcrLevel2 β hβ w).carrier (bcrLevel2 β hβ w).metric
          (bcrLevel2 β hβ w).s (bcrLevel2 β hβ w).t 0 cHi
          (α * (w : ℝ) ^ 2 * ((β : ℝ) * 3 ^ w)) price M),
        0 ≤ price ∧ (∀ ω₁ ω₂ : C.Ω, C.hist 0 ω₁ = C.hist 0 ω₂) := by sorry

end KServer
Source
Bubeck--Coester--Rabani, STOC 2023, Lemma 12 (arXiv:2211.05753)

View graph