The Blocking Lemma (Gale--Sotomayor)
ProvedAGT.blocking_lemmaThe Blocking Lemma of Gale and Sotomayor. Fix a two-sided market with a finite set of men and a finite set of women, each agent holding a strict ordering of the opposite side, and let matchings be bijections .
Let be a male-optimal stable matching: it is stable, and every man weakly prefers it to his partner in any other stable matching. Let be an arbitrary matching — no stability is assumed of it — and put
the set of men who strictly prefer to the male-optimal stable matching. Assume , witnessed by a man .
The lemma asserts that is then blocked by a pair drawn from outside on the man's side and from inside on the woman's side: there exist men and with and such that the pair blocks , i.e.
The point of the statement is the location of the blocking pair. That an unstable has some blocking pair is immediate from male-optimality once some man prefers ; what the lemma adds is that one can always find a blocking man who does not belong to , paired with a woman who is matched under to a member of . This is exactly the form in which the lemma is used to prove that the male-propose deferred-acceptance mechanism is strategy-proof for the men: a single man's misreport can only create blocking pairs involving himself, while the lemma produces a blocking pair involving somebody else.
The standard proof splits on whether . When the two sets of women differ, a woman in together with her -partner furnishes the pair directly, using only stability of . When they coincide, the hybrid matching that follows on and elsewhere is a matching that all men of strictly prefer to , and the conclusion is extracted from the deferred-acceptance run producing .
import Definitions.Def_agt_matching
namespace AGT
/-- **The Blocking Lemma** (Gale–Sotomayor 1985; Roth–Sotomayor, *Two-Sided
Matching*, Lemma 3.5). Let `mu` be a male-optimal stable matching for the strict
profiles `PM`, `PW`, let `nu` be an arbitrary matching, and let
`R = {m | PM m (nu m) (mu m)}` be the set of men who strictly prefer `nu` to `mu`.
If `R` is nonempty, witnessed by `m₀`, then `nu` is blocked by a pair `(m, nu m')`
with `m'` in `R` (so the blocking woman lies in `nu '' R`) and `m` outside `R`. -/
theorem blocking_lemma {M W : Type*} [Fintype M] [Fintype W]
(PM : M → W → W → Prop) (PW : W → M → M → Prop)
(hM : IsPrefProfile PM) (hW : IsPrefProfile PW)
(mu nu : M ≃ W) (hmu : IsMaleOptimal PM PW mu)
(m₀ : M) (hm₀ : PM m₀ (nu m₀) (mu m₀)) :
∃ m m' : M, PM m' (nu m') (mu m') ∧ ¬ PM m (nu m) (mu m) ∧
IsBlockingPair PM PW nu m (nu m') := by
sorry
end AGT