Proof of Lemma 4.2, p. 555 — existence of the refined mapping π on each $N_O(o)$

Proved

LocalSearchFL.UFL.exists_refined_pi

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

combinatoricslocal-searchp2o-batch-p100ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $\sigma_S, \sigma_O : C \to F$ be any two assignments of the clients to facilities, with $N_S(s) = \sigma_S^{-1}(s)$ , $N_O(o) = \sigma_O^{-1}(o)$ and $N^o_s = N_O(o) \cap N_S(s)$ . Then there is a permutation $\pi$ of $C$ such that

$\pi$ maps every $N_O(o)$ onto itself;
(Property 3.1) whenever $|N^o_s| \le \tfrac12 |N_O(o)|$ , $\pi(N^o_s) \cap N^o_s = \emptyset$ ;
whenever $|N^o_s| > \tfrac12 |N_O(o)|$ , every $j \in N^o_s$ with $\pi(j) \in N^o_s$ satisfies $\pi(j) = j$ .

This is the mapping on which the facility cost bound of Lemma 4.2 is built: a client whose serving facility in $S$ is closed is reassigned through $\pi$ , and the fixed points of $\pi$ are exactly the clients of a captured block that cannot be moved to another block.

Formalization Note The family of bijections $\pi : N_O(o) \to N_O(o)$ , one for each $o$ , is encoded as a single permutation of all clients with $\sigma_O \circ \pi = \sigma_O$ . The assignments are arbitrary maps: the statement is purely combinatorial.

Preamble

import Mathlib
import Definitions.Def_LocalSearchFL_UFL_captures

Formal statement

namespace LocalSearchFL.UFL

/-- The mapping π of the proof of Lemma 4.2 (p. 555, first paragraph of the proof): for any
assignments `σS`, `σO` of the clients, there is a permutation `π` of the clients that maps each
`N_O(o)` onto itself, satisfies Property 3.1 (if `s` does not capture `o` then
`π(N^o_s) ∩ N^o_s = ∅`), and, when `s` captures `o`, fixes every `j ∈ N^o_s` with
`π(j) ∈ N^o_s`. -/
theorem exists_refined_pi {Cl Fa : Type} [Fintype Cl] [DecidableEq Cl] [DecidableEq Fa]
    (σS σO : Cl → Fa) :
    ∃ π : Equiv.Perm Cl, IsRefinedPi σS σO π := 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. 555, proof of Lemma 4.2, first paragraph (with Property 3.1 and its construction, p. 549)

Read-back

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

Setting. Let $\mathcal C$ be a finite type of clients with decidable equality. Let $\mathcal F$ be any type of facilities with decidable equality; it need not be finite. Let $\sigma_S,\sigma_O:\mathcal C\to\mathcal F$ be arbitrary maps. Write:

$N_O(o)=\{j:\sigma_O(j)=o\}$ and $N_S(s)=\{j:\sigma_S(j)=s\}$ ;
$N^o_s=N_O(o)\cap N_S(s)$ .

Say that $s$ captures $o$ when $|N_O(o)|<2|N^o_s|$ , as a strict inequality of natural numbers.

Conclusion. For every such pair of maps, there exists a bijection $\pi:\mathcal C\to\mathcal C$ satisfying all three of:

(i) $\sigma_O(\pi(j))=\sigma_O(j)$ for every client $j$ ;
(ii) for all facilities $s,o$ such that $s$ does not capture $o$ , and every $j\in N^o_s$ : $\pi(j)\notin N^o_s$ ;
(iii) for all facilities $s,o$ such that $s$ captures $o$ , and every $j\in N^o_s$ with $\pi(j)\in N^o_s$ : $\pi(j)=j$ .

No distances, costs or sets of open facilities appear in the statement. The maps $\sigma_S,\sigma_O$ are completely unrestricted.

Degenerate cases.

If $\mathcal C=\emptyset$ , the empty permutation witnesses the claim.
If $\mathcal C$ has one client $j$ , then $N_O(\sigma_O(j))=\{j\}$ is captured by $\sigma_S(j)$ , and the identity satisfies (i)–(iii).
In general, the claim includes every client $j$ whose own pair $(\sigma_S(j),\sigma_O(j))$ is uncaptured. For each such $j$ , it asserts that $\pi$ moves $j$ to a client with the same $\sigma_O$ -value but a different $\sigma_S$ -value.

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

Proof of Lemma 4.2, p. 555 — existence of the refined mapping π on each NO(o)N_O(o)NO​(o)

Proof of Lemma 4.2, p. 555 — existence of the refined mapping π on each $N_O(o)$