Inequality (6) — swapping a bad facility with its nearest captured facility

Proved

LocalSearchFL.UFL.swap_bad_inequality_6

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

facility-locationlocal-searchp2o-batch-p100ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $f_i \ge 0$ be facility opening costs on a metric instance, let $S$ be a nonempty set of facilities that is locally optimum for the add/drop/swap neighbourhood (4), and let $O$ be any solution. Let $\sigma_S$ , $\sigma_O$ be nearest-facility assignments for $S$ and $O$ , write $S_j = c_{j\sigma_S(j)}$ and $O_j = c_{j\sigma_O(j)}$ , and let $\pi$ be a permutation of the clients satisfying the three conditions of the mapping of the proof of Lemma 4.2.

Let $s \in S$ capture $o \in O$ , where $o$ is nearest to $s$ among the facilities of $O$ captured by $s$ : $c_{so} \le c_{so'}$ for every $o' \in O$ captured by $s$ . Then

\begin{aligned} f_o - f_s &+ \sum_{\substack{j \in N_S(s)\\ \pi(j) \neq j}} \bigl(O_j + O_{\pi(j)} + S_{\pi(j)} - S_j\bigr) \\ &+ \sum_{\substack{j \in N_O(o),\\ \pi(j) = j \in N_S(s)}} (O_j - S_j) + \sum_{\substack{j \notin N_O(o),\\ \pi(j) = j \in N_S(s)}} (S_j + S_j + O_j - S_j) \ \ge\ 0. \end{aligned}

This is the information extracted from the swap $\langle s, o\rangle$ that closes a bad facility $s$ and opens $o$ ; it is the main ingredient of inequality (8).

Formalization Note The distance $c_{so}$ between two facilities is I.cf s o. The summand $S_j + S_j + O_j - S_j$ is kept in the paper's unsimplified form.

Preamble

import Mathlib
import Definitions.Def_LocalSearchFL_UFL_captures

Formal statement

namespace LocalSearchFL.UFL

/-- Inequality (6), pp. 555–556: the swap `⟨s, o⟩` for a bad facility. Let `S` be a locally
optimum solution for the neighbourhood (4), `O` any solution, `σS`, `σO` nearest-facility
assignments, `π` the mapping of the proof of Lemma 4.2. Let `s ∈ S` capture `o ∈ O`, where `o`
is a facility nearest to `s` among the facilities of `O` captured by `s`
(`c_{so} ≤ c_{so'}` for every `o' ∈ O` captured by `s`). Then
`f_o − f_s + ∑_{j ∈ N_S(s), π(j) ≠ j} (O_j + O_{π(j)} + S_{π(j)} − S_j)
  + ∑_{j ∈ N_O(o), π(j) = j ∈ N_S(s)} (O_j − S_j)
  + ∑_{j ∉ N_O(o), π(j) = j ∈ N_S(s)} (S_j + S_j + O_j − S_j) ≥ 0`. -/
theorem swap_bad_inequality_6 {Cl Fa : Type} [Fintype Cl] [DecidableEq Cl]
    [Fintype Fa] [DecidableEq Fa]
    (I : MetricInstance Cl Fa) (f : Fa → ℝ) (hf : ∀ i, 0 ≤ f i)
    (S O : Finset Fa) (hS : S.Nonempty) (hloc : IsUFLLocalOpt I f S hS)
    (σS σO : Cl → Fa) (hσS : IsNearestAssignment I S σS) (hσO : IsNearestAssignment I O σO)
    (π : Equiv.Perm Cl) (hπ : IsRefinedPi σS σO π)
    (s o : Fa) (hs : s ∈ S) (ho : o ∈ O) (hcap : captures σS σO s o)
    (hnearest : ∀ o' ∈ O, captures σS σO s o' → I.cf s o ≤ I.cf s o') :
    0 ≤ f o - f s +
      ∑ j ∈ (nbhd σS s).filter (fun j => π j ≠ j),
        (I.c j (σO j) + I.c (π j) (σO (π j)) + I.c (π j) (σS (π j)) - I.c j (σS j)) +
      ∑ j ∈ (nbhd σS s).filter (fun j => π j = j ∧ σO j = o),
        (I.c j (σO j) - I.c j (σS j)) +
      ∑ j ∈ (nbhd σS s).filter (fun j => π j = j ∧ σO j ≠ o),
        (I.c j (σS j) + I.c j (σS j) + I.c j (σO j) - I.c j (σS j)) := 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, pp. 555–556, eq. (6)

Read-back

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

Setting. Let $\mathcal C$ (clients) and $\mathcal F$ (facilities) be finite types with decidable equality. Let $I$ be a metric instance: $d$ on pairs of points of $\mathcal C\sqcup\mathcal F$ , nonnegative, symmetric, triangle inequality, self-distance not assumed zero. Write $c_{ji}=d(j,i)$ for a client and a facility, and $c_{ii'}=d(i,i')$ for two facilities. Let $f:\mathcal F\to\mathbb R$ satisfy $f_i\ge0$ for all $i$ . For nonempty $A\subseteq\mathcal F$ , write $\mathrm{cost}(A)=\sum_{i\in A}f_i+\sum_{j\in\mathcal C}\min_{i\in A}c_{ji}$ .

Hypotheses.

$S,O$ are finite sets of facilities, and $S$ is nonempty.
$S$ is locally optimal:
- $\mathrm{cost}(S)\le\mathrm{cost}(S\cup\{s'\})$ for every facility $s'$ ;
- $\mathrm{cost}(S)\le\mathrm{cost}(S\setminus\{s\})$ for every $s\in S$ with $S\setminus\{s\}\ne\emptyset$ ;
- $\mathrm{cost}(S)\le\mathrm{cost}((S\setminus\{s\})\cup\{s'\})$ for all $s\in S$ and all facilities $s'$ .
$\sigma_S,\sigma_O:\mathcal C\to\mathcal F$ are nearest-facility assignments:
- for every $j$ : $\sigma_S(j)\in S$ and $c_{j\sigma_S(j)}=\min_{i\in S}c_{ji}$ ;
- for every $j$ : $\sigma_O(j)\in O$ and $c_{j\sigma_O(j)}=\min_{i\in O}c_{ji}$ .
Write $S_j=c_{j\sigma_S(j)}$ and $O_j=c_{j\sigma_O(j)}$ .
Write $N_S(s)=\{j:\sigma_S(j)=s\}$ , $N_O(o)=\{j:\sigma_O(j)=o\}$ and $N^o_s=N_O(o)\cap N_S(s)$ . Say that $s$ captures $o$ when $|N_O(o)|<2|N^o_s|$ .
$\pi$ is a permutation of $\mathcal C$ satisfying all three of:
- (i) $\sigma_O(\pi(j))=\sigma_O(j)$ for all $j$ ;
- (ii) for all facilities $s,o$ with $s$ not capturing $o$ : $j\in N^o_s\Rightarrow\pi(j)\notin N^o_s$ ;
- (iii) for all facilities $s,o$ with $s$ capturing $o$ : $j,\pi(j)\in N^o_s\Rightarrow\pi(j)=j$ .
$s\in S$ and $o\in O$ , and $s$ captures $o$ .
For every $o'\in O$ that $s$ captures: $c_{so}\le c_{so'}$ .

Conclusion.

0\le f_o-f_s+\sum_{\substack{j\in N_S(s)\\ \pi(j)\ne j}}\big(O_j+O_{\pi(j)}+S_{\pi(j)}-S_j\big)+\sum_{\substack{j\in N_S(s),\ \pi(j)=j\\ \sigma_O(j)=o}}\big(O_j-S_j\big)+\sum_{\substack{j\in N_S(s),\ \pi(j)=j\\ \sigma_O(j)\ne o}}\big(S_j+S_j+O_j-S_j\big),

where $O_{\pi(j)}=c_{\pi(j)\sigma_O(\pi(j))}$ and $S_{\pi(j)}=c_{\pi(j)\sigma_S(\pi(j))}$ . The summand of the last sum is algebraically $S_j+O_j$ .

Degenerate cases.

Capture forces $|N^o_s|\ge1$ . So $\mathcal C$ is nonempty, and $s$ serves at least one client assigned to $o$ .
If $s$ captures only $o$ within $O$ , the nearest-captured condition holds trivially.
If $o\in S$ as well, the facility cost $f_o$ still appears in the conclusion.

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