# The metric <i>k</i>-median approximation threshold and recovery

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

- [Single-exponential recovery and bounded-price strictness for metric $k$-median](../../preprints/Single-Exponential-Recovery-and-Bounded-Price-Strictness-for-Metric-k-Median-September-24-2026/paper.pdf)
- [The approximation threshold for metric $k$-median](../../preprints/The-Approximation-Threshold-for-Metric-k-Median-September-24-2026/main.pdf)

## Scope

The formalization gives an exact-budget recovery algorithm for metric $k$-median on the stated polynomially bounded integral metrics. Suppose a supplied anchor represents all but logarithmically many comparison clusters by distinct proxies, with total proxy cost at most the comparison cost plus a sufficiently small relative error. The algorithm always opens at most $k$ facilities and, with any requested confidence, attains a $(1+2/e+\varepsilon)$ factor relative to those comparison centers in polynomial time.

The linked final approximation result applies to arbitrary finite rational metrics. For one absolute $\sigma>0$, a polynomial-time fair-bit algorithm always returns a feasible solution, has expected cost at most $(2-\sigma)\mathrm{OPT}$, and attains the same factor with arbitrarily high polynomial confidence.

The formalization gives, for every fixed $\varepsilon>0$, a deterministic polynomial-time $(1+2/e+\varepsilon)$-approximation for metric $k$-median on finite rational metrics with specified candidate facilities. Every output is a nonempty subset of the candidate facilities and opens at most $k$ of them.

Assuming $P\ne NP$, it also proves that the infimum of all polynomial-time approximation factors in this model is exactly $1+2/e$.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Randomized metric $k$-median approximation below two | [KMedianRecovery.lean](../ComparatorChallenges/KMedianRecovery.lean) |
| Exact-budget recovery from accurate distinct cluster proxies | [KMedianRefinedRecovery.lean](../ComparatorChallenges/KMedianRefinedRecovery.lean) |
| Exact approximation threshold under $P\ne NP$ | [KMedianThreshold.lean](../ComparatorChallenges/KMedianThreshold.lean) |
| Deterministic metric $k$-median approximation at the threshold | [MetricKMedian.lean](../ComparatorChallenges/MetricKMedian.lean) |