Path-space base chunk system with a free escape price
ProvedKServer.chunk_system_b_base2The base case of the BCR chunk induction, with the escape price as a free parameter. On the path metric on (consecutive points at distance ), the marked endpoints are at distance , and for any and level with , and any escape price , there is a chunk system between the endpoints with deterministic outcomes, sizes in , at least chunks, expected total at least , and per-chunk conditional cost claims financed by the escape price . The cruel single-file request pattern forces cost per chunk however the evader plays, and bailing at any prefix costs the full price , so any price of at least one unit is sound. Freeing the price from the previously fixed value lets the level recursion carry a price on the chunk-size scale, as required by the coin-phase separation arithmetic of the race construction.
import Mathlib import Definitions.Def_KServer_evader import Definitions.Def_KServer_chunk_system import Definitions.Def_KServer_chunk_system_f import Definitions.Def_KServer_evader_bail import Definitions.Def_KServer_chunk_system_b
namespace KServer
theorem chunk_system_b_base2 (β : ℕ) (hβ : 1 ≤ β) (α : ℝ) (hα0 : 0 ≤ α) (w : ℕ)
(hw : α * (w : ℝ) ^ 2 ≤ 1) (p : ℝ) (hp : 1 ≤ p) :
letI := pathMetric β
dist (0 : Fin (β + 1)) (Fin.last β) = β ∧
Nonempty (ChunkSystemB (Fin (β + 1)) 0 (Fin.last β)
(1 / 2) (3 / 2) (α * (w : ℝ) ^ 2 * β) p ⌈α * β * (w : ℝ) ^ 2⌉₊) := by sorry
end KServer