A chunk of a chunk system has size at most the escape price

Proved

KServer.chunk_size_le_price

by Gabewhigham · Sep 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

competitive-analysisk-serveronline-algorithms

Let $C$ be a chunk system with online escapes with escape price $p_e\\ge0$ . Then every chunk of $C$ has size at most the escape price:

c_i(\\omega)\\;\\le\\;p_e\\qquad\\text{for all outcomes }\\omega\\text{ and all chunk indices }i.

Why. The cost axiom of a chunk system holds against every online escape rule, in particular against the rule that escapes immediately, before serving the first request of the current chunk. That rule lets any evader off for exactly the escape price, so the conditional cost that the axiom charges to a chunk is at most $p_e$ , and the size of the chunk is bounded by it.

Consequence. In any satisfiable chunk system the size floor is at most the escape price, so a chunk-level statement demanding a size floor larger than its escape price is vacuous. This is the basic consistency constraint tying the two parameters of the induction together.

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_chunk_cond

Formal statement

namespace KServer

theorem chunk_size_le_price {X : Type*} [MetricSpace X] {s t : X}
    {cLo cHi total price : ℝ} {mL : ℕ} (C : ChunkSystemB X s t cLo cHi total price mL)
    (hp : 0 ≤ price) (ω : C.Ω) (i : Fin C.m) : C.size ω i ≤ price := by sorry

end KServer

View graph