Prove2Me
Navigate
MissionsFormalpediaBlogsUsersMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Sequential composition of chunk systems at a geodesic junction

Proved
KServer.chunk_system_seq

by Shuze Chen · Sep 1, 2026 · Mathlib c5ea003 (Lean v4.30.0)

k-serverlower-boundmetrical-service-systemsonline-algorithms

Sequential composition of chunk systems at a geodesic junction. Let YYY be a metric space and a,b,c∈Ya, b, c \in Ya,b,c∈Y with d(a,b)+d(b,c)≤d(a,c)d(a,b) + d(b,c) \le d(a,c)d(a,b)+d(b,c)≤d(a,c) (so bbb lies on a geodesic from aaa to ccc). Let C1C_1C1​ be a chunk system with online escapes from aaa to bbb and C2C_2C2​ one from bbb to ccc, at a common escape price pe≥0p_e \ge 0pe​≥0, with trivial initial histories and size-total variances at most V1V_1V1​ and V2V_2V2​. Then on the product sample space there is a chunk system from aaa to ccc whose request sequence is the concatenation of the two phases, with the concatenated chunks and sizes, expected total T1+T2T_1 + T_2T1​+T2​, chunk count m1+m2m_1 + m_2m1​+m2​, any size window containing both input windows, trivial initial history, and variance at most V1+V2V_1 + V_2V1​+V2​:

Var(∑ici)≤V1+V2,\mathrm{Var}\Big(\sum_i c_i\Big) \le V_1 + V_2,Var(i∑​ci​)≤V1​+V2​,

by independence of the two phases. The two-phase filtration reveals the first system's history verbatim, then pairs its complete history with the running second-phase history; the second phase's cost premises transfer to the composite by conditioning each evader on the fixed first-phase request prefix, and the offline bound concatenates because the first sequence ends with the pinned singleton request {b}\{b\}{b}. This combinator chains the stage constructions of the BCR lower-bound induction along the junctions of the glued level step.

Preamble
import Mathlib
import Definitions.Def_KServer_evader
import Definitions.Def_KServer_evader_bail
import Definitions.Def_KServer_chunk_system_b
import Definitions.Def_KServer_bail_append
import Definitions.Def_KServer_shadow
Formal statement
namespace KServer

theorem chunk_system_seq {Y : Type*} [MetricSpace Y] {a b c : Y}
    {cA1 cB1 cA2 cB2 T1 T2 pe : ℝ} {mL1 mL2 : ℕ}
    (C1 : ChunkSystemB Y a b cA1 cB1 T1 pe mL1)
    (C2 : ChunkSystemB Y b c cA2 cB2 T2 pe mL2)
    {cLo cHi V1 V2 : ℝ}
    (hgeo : dist a b + dist b c ≤ dist a c)
    (hpe : 0 ≤ pe)
    (hlo1 : cLo ≤ cA1) (hlo2 : cLo ≤ cA2)
    (hhi1 : cB1 ≤ cHi) (hhi2 : cB2 ≤ cHi)
    (h0triv1 : ∀ ω₁ ω₂ : C1.Ω, C1.hist 0 ω₁ = C1.hist 0 ω₂)
    (h0triv2 : ∀ ω₁ ω₂ : C2.Ω, C2.hist 0 ω₁ = C2.hist 0 ω₂)
    (hVar1 : ∑ ω, C1.P ω * ((∑ i, C1.size ω i)
      - ∑ ω', C1.P ω' * ∑ i, C1.size ω' i) ^ 2 ≤ V1)
    (hVar2 : ∑ ω, C2.P ω * ((∑ i, C2.size ω i)
      - ∑ ω', C2.P ω' * ∑ i, C2.size ω' i) ^ 2 ≤ V2) :
    ∃ C' : ChunkSystemB Y a c cLo cHi (T1 + T2) pe (mL1 + mL2),
      (∀ ω₁ ω₂ : C'.Ω, C'.hist 0 ω₁ = C'.hist 0 ω₂) ∧
      (∑ ω, C'.P ω * ((∑ i, C'.size ω i)
          - ∑ ω', C'.P ω' * (∑ i, C'.size ω' i)) ^ 2 ≤ V1 + V2) := by sorry

end KServer
Source
BCR randomized k-server lower bound, stage construction layer

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactJoin Slack© 2026 Prove2Me