The base case: a chunk system on the path
ProvedKServer.chunk_system_baseThe base case of BCR's Lemma 6: on the path of equally spaced points (with , , so ), whenever there is a (deterministic) chunk system with chunks: after an initial pinning request , the -th chunk is the single request , of size . The total size dominates , and .
The conditional cost bound holds against every evader with escape price : after serving the requests the evader's position is pinned at , so serving costs exactly , while bailing out costs ; the first chunk costs at least from any starting position because it pins the evader at before requesting . The offline evader serves everything for cost by walking down the path.
Role
This is the induction base of the Bubeck–Coester–Rabani lower bound (STOC 2023, Section 4): all levels with use this path system; the six-copy cyclic construction then builds the higher levels.
Formalization note
The path metric is induced from the embedding into ℝ. The first chunk is rather than , pinning the start (the evader model has no distinguished starting point); the sequence convention "first request " matches BCR.
import Mathlib import Definitions.Def_KServer_evader import Definitions.Def_KServer_chunk_system
namespace KServer
theorem chunk_system_base (β : ℕ) (hβ : 1 ≤ β) (α : ℝ) (hα0 : 0 ≤ α) (w : ℕ)
(hw : α * (w : ℝ) ^ 2 ≤ 1) :
letI := pathMetric β
dist (0 : Fin (β + 1)) (Fin.last β) = β ∧
Nonempty (ChunkSystem (Fin (β + 1)) 0 (Fin.last β)
(1 / 2) (3 / 2) (α * (w : ℝ) ^ 2 * β) (2 * β) ⌈α * β * (w : ℝ) ^ 2⌉₊) := by sorry
end KServer