Theorem 6 — $c^*$ is realizable iff $\sum_i 1/c(i)\le 1$

Proved

CompetitivePaging.Combining.realizable_iff

by mikedeng1 · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

competitive-analysisonline-algorithmsp2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1paging

Let $m\ge1$ and let $c^*=(c(1),\dots,c(m))$ be a sequence of positive reals. Then $c^*$ is realizable — for every type $(k,n)$ of paging algorithm and every $m$ deterministic on-line algorithms $B(1),\dots,B(m)$ of that type there is one deterministic on-line algorithm $A$ of the same type that is $c(i)$ -competitive against each $B(i)$ — if and only if

\sum_{1\le i\le m}\frac{1}{c(i)}\le 1 .

For example, with $m=2$ and $c(1)=c(2)=2$ any two paging algorithms can be combined into one that costs at most twice either of them, up to an additive constant, while no pair of ratios with $1/c(1)+1/c(2)>1$ can be achieved against every pair of algorithms.

Formalization Note Realizability quantifies over every type: every $k\in\mathbb N$ and every finite type $M$ with the uniform metric. The hypothesis $m\ge1$ is the paper's ("let $m$ be a positive integer"); for $m=0$ the realizability of the empty sequence would demand an algorithm of every type, which does not exist for $k=0$ servers on a nonempty vertex set.

Preamble

import Mathlib
import Definitions.Def_KServer_model
import Definitions.Def_CompetitivePaging_Combining_Realizable

Formal statement

namespace CompetitivePaging.Combining

/-- **Theorem 6** (Fiat, Karp, Luby, McGeoch, Sleator, Young 1991, p. 9). A sequence
`c = (c(1), …, c(m))` of positive reals is realizable if and only if `∑_{i} 1 / c(i) ≤ 1`. -/
theorem realizable_iff {m : ℕ} (hm : 0 < m) (c : Fin m → ℝ) (hc : ∀ i, 0 < c i) :
    Realizable c ↔ ∑ i, 1 / c i ≤ 1 := by sorry

end CompetitivePaging.Combining

Source

Fiat, Karp, Luby, McGeoch, Sleator, Young, Competitive Paging Algorithms, arXiv:cs/0205038v1, p. 9 (PDF p. 10), Theorem 6, eq. (1)

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Fix a natural number $m$ with $m > 0$ . Let $c = (c_1, \dots, c_m)$ be a finite sequence of real numbers indexed by $\{1, \dots, m\}$ , and assume every entry is strictly positive:

c_i > 0 \quad \text{for every } i \in \{1, \dots, m\}.

The statement asserts a two-way equivalence: $c$ satisfies the predicate $\mathrm{Realizable}$ if and only if the sum of the reciprocals of its entries is at most $1$ :

\mathrm{Realizable}(c) \iff \sum_{i=1}^{m} \frac{1}{c_i} \le 1 .

The predicate $\mathrm{Realizable}$ is defined in an imported module (the Definitions.Def_CompetitivePaging_Combining_Realizable file, namespace CompetitivePaging.Combining). That module's code is not part of the declaration I was given, so I cannot expand it here. The meaning of the left-hand side depends entirely on that definition. In particular, the statement itself does not say what "realizable" means: whether it involves paging, the $k$ -server model (also imported), competitive ratios, or anything else. The statement uses a non-strict inequality ( $\le 1$ , not $< 1$ ), and each side both implies and is implied by the other. The doc comment before the theorem (about Theorem 6 of Fiat, Karp, Luby, McGeoch, Sleator and Young, 1991) describes what the author intends. It is not part of what the code asserts.

Degenerate cases. The hypothesis $m > 0$ rules out the empty sequence. For $m = 0$ the sum would have been $0$ , but that case is excluded, so the statement says nothing about it. The hypothesis $c_i > 0$ rules out division by zero, so none of the reciprocals falls back to a default value. With only one entry ( $m = 1$ ), the statement says that $(c_1)$ is realizable exactly when $1/c_1 \le 1$ , which means exactly when $c_1 \ge 1$ . More generally, the right-hand side can only hold if every $c_i \ge 1$ , because each term $1/c_i$ is positive and would exceed $1$ on its own otherwise. The hypotheses can always be satisfied (for example, $m = 1$ and $c_1 = 1$ ), so the theorem is not vacuous. The statement fixes nothing about the value of $\mathrm{Realizable}(c)$ for sequences that have a zero or negative entry: such sequences are outside its hypotheses.

Human review

Endorsed by Shuze Chen · Sep 27, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Sep 27, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Theorem 6 — c∗c^*c∗ is realizable iff ∑i1/c(i)≤1\sum_i 1/c(i)\le 1∑i​1/c(i)≤1

Theorem 6 — $c^*$ is realizable iff $\sum_i 1/c(i)\le 1$