Theorem 4.1: pathwise feasibility clause

For every $n$ and integer capacity $k\ge1$, every arrival permutation $\sigma$, every online activation vector $X$, every sample vector $Y$, and either value of the coin $Q$, Algorithm 4's defined run satisfies

This is the pathwise feasibility clause of Theorem 4.1. It requires no distributional assumptions, because it holds for every realization, including realizations of probability zero.

Differences from the source:

• encoding: the labeled set [n] = {1,…,n} → Fin n = {0,…,n−1}; reason: relabeling preserves each element and its arrival rank
• encoding: the standing assumption k ≥ 1 in §2, p.5 → an explicit hypothesis 1 ≤ k; reason: Lean natural numbers include zero