Theorem 4.3: add/drop/swap local search for metric UFL has locality gap at most 3

Proved

LocalSearchFL.UFL.ufl_locality_gap

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

approximation-algorithmsfacility-locationlocal-searchp2o-batch-p100ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $C$ be a finite set of clients and $F$ a finite set of facilities, with a distance on $C \cup F$ that is nonnegative, symmetric and satisfies the triangle inequality, and let $c_{ji}$ be the cost of serving client $j$ by facility $i$ . Each facility $i$ has an opening cost $f_i \ge 0$ . The cost of a nonempty set $S \subseteq F$ of open facilities is

\mathrm{cost}(S) = \sum_{i \in S} f_i + \sum_{j \in C} \min_{i \in S} c_{ji}.

$S$ is locally optimum for the neighbourhood

\mathcal B(S) = \{S + \{s'\}\} \cup \{S - \{s\} \mid s \in S\} \cup \{S - \{s\} + \{s'\} \mid s \in S\}

if no neighbour has smaller cost.

Theorem 4.3. If $S$ is locally optimum for $\mathcal B$ , then for every nonempty $O \subseteq F$ ,

\mathrm{cost}(S) \le 3 \cdot \mathrm{cost}(O).

In words: the local search procedure that adds, drops or swaps one facility at a time has locality gap at most 3 for the metric uncapacitated facility location problem. The bound is tight (§4.3 of the paper).

Formalization Note The locality gap bound is stated as the inequality for every local optimum $S$ and every solution $O$ (not only an optimal one), multiplied out rather than as a ratio. Only nonempty sets are solutions; the drop move is considered only when a facility remains open.

Preamble

import Mathlib
import Definitions.Def_LocalSearchFL_UFL_captures

Formal statement

namespace LocalSearchFL.UFL

/-- Theorem 4.3, p. 557: local search for the metric UFL problem with the neighbourhood
`B(S) = {S + {s'}} ∪ {S − {s} | s ∈ S} ∪ {S − {s} + {s'} | s ∈ S}` has locality gap at most 3:
if `S` is locally optimum for `B`, then `cost(S) ≤ 3 · cost(O)` for every solution `O`. -/
theorem ufl_locality_gap {Cl Fa : Type} [Fintype Cl] [DecidableEq Cl]
    [Fintype Fa] [DecidableEq Fa]
    (I : MetricInstance Cl Fa) (f : Fa → ℝ) (hf : ∀ i, 0 ≤ f i)
    (S : Finset Fa) (hS : S.Nonempty) (hloc : IsUFLLocalOpt I f S hS)
    (O : Finset Fa) (hO : O.Nonempty) :
    uflCost I f S hS ≤ 3 * uflCost I f O hO := by sorry

end LocalSearchFL.UFL

Source

Arya, Garg, Khandekar, Meyerson, Munagala, Pandit, Local Search Heuristics for k-Median and Facility Location Problems, SIAM J. Comput. 33(3), 2004, p. 557, Theorem 4.3

Read-back

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

Let $\mathcal{C}$ and $\mathcal{F}$ be arbitrary types, both finite and with decidable equality. The statement takes these as parameters:

$I$ , a value of type MetricInstance built on $\mathcal{C}$ and $\mathcal{F}$ . This type comes from the imported bundle Definitions.Def_LocalSearchFL_UFL_captures, and its definition is not included in the code under audit. Nothing here fixes what data $I$ holds (for example, distances between elements of $\mathcal{C}$ and $\mathcal{F}$ ) or what conditions it imposes (for example, non-negativity or a triangle inequality).
$f : \mathcal{F} \to \mathbb{R}$ , a real-valued function on $\mathcal{F}$ , with the hypothesis that $f(i) \ge 0$ for every $i \in \mathcal{F}$ .
$S \subseteq \mathcal{F}$ , a finite set with a proof $h_S$ that $S \neq \emptyset$ .
A hypothesis that $S$ satisfies $\mathrm{IsUFLLocalOpt}(I, f, S, h_S)$ . This predicate comes from the same imported bundle and is not shown. The code does not reveal which neighbouring sets it compares $S$ against, how it compares them, or whether that comparison can involve empty sets.
$O \subseteq \mathcal{F}$ , a second finite set with a proof $h_O$ that $O \neq \emptyset$ .

The conclusion is

\mathrm{cost}_{I,f}(S) \;\le\; 3 \cdot \mathrm{cost}_{I,f}(O),

where $\mathrm{cost}_{I,f}(X)$ is the imported function uflCost applied to $I$ , $f$ , the set $X$ and its non-emptiness proof. Its definition is also not shown, so the code does not reveal how it combines $f$ with the data in $I$ . The set $O$ is universally quantified: it can be any non-empty subset of $\mathcal{F}$ , with no optimality condition on it. The inequality is non-strict ( $\le$ ), and the constant is exactly $3$ .

Degenerate cases:

$\mathcal{F}$ is empty. Then no non-empty $S$ exists, and the statement holds vacuously.
$\mathcal{F}$ has exactly one element. Then $S = O$ is that single element, and the claim becomes $\mathrm{cost}(S) \le 3\,\mathrm{cost}(S)$ . This is true exactly when that cost is non-negative, which depends on the unseen definitions of uflCost and MetricInstance.
$\mathcal{C}$ is empty. The statement does not exclude this. What the cost then equals depends on the unseen definition of uflCost.
$S$ fails the local-optimality predicate. Then the statement asserts nothing about $S$ . It holds vacuously for every such $S$ , and in general if the predicate can never be satisfied.
Total-function defaults. Whether division by zero, a minimum over an empty set, or another default value can occur inside uflCost or IsUFLLocalOpt cannot be determined from the code shown.

The only explicit hypothesis on $f$ is non-negativity. Nothing in the visible code requires $f$ to be positive or bounded above.

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