# Optimal-order randomized <i>k</i>-server on arbitrary metrics

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [Squared-logarithmic randomized $k$-server on arbitrary metrics](../../preprints/Squared-logarithmic-randomized-k-server-on-arbitrary-metrics-September-24-2026/Squared-logarithmic-randomized-k-server-on-arbitrary-metrics-September-24-2026.pdf)
- [Uniform computation of the squared-logarithmic $k$-server bound](../../preprints/Uniform-computation-of-the-squared-logarithmic-k-server-bound-September-24-2026/Uniform-computation-of-the-squared-logarithmic-k-server-bound-September-24-2026.pdf)

## Scope

The formalization proves an $O((\log(k+1))^2)$ competitive ratio for randomized $k$-server against oblivious finite request sequences. For every $k\ge2$, every metric space containing at least $k+1$ points, and every initial configuration, one policy works for all request sequences, including in infinite and unbounded spaces.

The bound permits a configuration-dependent additive constant, which is zero when the initial server positions are distinct. The universal multiplicative constant is independent of the metric and $k$.

The formalization constructs one uniform randomized bit algorithm for $k$-server on finite rational metrics, for $2\le k<n$. Its expected movement on every oblivious finite request sequence is at most an absolute multiple of $(\log(k+1))^2$ times the offline optimum, plus a finite instance-dependent additive constant.

Preprocessing is polynomial in the encoded input length, and each request is processed in time polynomial in that length and the binary length of the request counter. Every processed request returns a legal server index. The additive movement constant is not claimed to be polynomially bounded.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Squared-logarithmic randomized $k$-server on arbitrary metrics | [KServer.lean](../ComparatorChallenges/KServer.lean) |
| Uniform bit algorithm for the squared-logarithmic $k$-server bound | [UniformKServer.lean](../ComparatorChallenges/UniformKServer.lean) |