EconCSLib.MarketDesign.Matching.Optimal

Men-optimal property of the men-proposing Gale–Shapley deferred-acceptance algorithm: every man's GS partner is at least as preferred (by him) as his partner in any other stable matching.

This is the proposer-side dominance result. The dual receiver-side pessimality result belongs with the lattice and Rural-Hospitals developments.

Main theorem

• galeShapley_isProposingOptimal — for every other stable matching μ pairing man j with wj (via μ.matchW j = some wj; recall the codebase convention M = women, W = men in MatchingMarket M W), the GS partner of j is ranked at most as high (i.e., as good or better) as wj in m.prefs j.

Proof strategy (Gale–Shapley 1962 / Gusfield–Irving 1989)

The standard achievable-partner argument. A pair (j, wj) is achievable if some stable matching pairs them (IsAchievable). The heart of the proof is the no-achievable-rejection invariant on the GS run state:

∀ j wj, IsAchievable j wj →
  (m.prefs j).idxOf wj < s.nextChoice j → s.holding wj = some j

— informally: "if man j has already proposed to woman wj and wj is achievable for him, then wj is currently holding j." Equivalently, no man has been rejected by any of his achievable partners.

Once this invariant holds at finalState, the main theorem follows mechanically: j's GS partner is in his proposed-prefix (by HoldInv), and any other achievable partner must either also be in the prefix (and then by injectivity = the GS partner), or lie strictly past the prefix (so it's a worse rank).

The inductive step daStep_NoAchievableRejection is the deep core (now proved): if at daStep man q displaces man j at woman wj (i.e., wj was holding j and switches to q), and wj is achievable for j via stable matching μ, then (q, wj) blocks μ — because the run invariant for s forces q to be free and to not yet have proposed past any of his μ-achievable partners, hence q strictly prefers wj over his μ-partner. The invariant carries HoldInv and holding-injectivity alongside (both preserved by daStep).

References

• [MSZ Theorem 22.10] Maschler, Solan, Zamir, Game Theory, §22.
• [Gale-Shapley 1962] Am. Math. Monthly 69(1):9–15 — original proof.
• [Gusfield-Irving 1989] The Stable Marriage Problem, MIT Press.
• [Roth-Sotomayor 1990] Two-Sided Matching, Cambridge, §2.2.

Achievability

def GS.IsAchievable {n : ℕ} (w m : Preferences n) (j wj : Fin n) : Prop

IsAchievable w m j wj says woman wj is achievable for man j: some stable matching pairs them. Recall the codebase convention MatchingMarket M W with M = women, W = men; man j's partner under μ is μ.matchW j.

Equations

• GS.IsAchievable w m j wj = ∃ (μ : Matching (Fin n) (Fin n)), Matching.IsStable (MatchingMarket.ofEquivData w m) μ ∧ μ.matchW j = some wj

theorem GS.gs_partner_isAchievable {n : ℕ} [NeZero n] (w m : Preferences n) (j : Fin n) : IsAchievable w m j ((Equiv.ofBijective (gs w m) ⋯).symm j)

The GS output itself witnesses that gs.symm j is achievable for j.

Run-state invariant: no rejection by an achievable partner

def GS.NoAchievableRejection {n : ℕ} (w m : Preferences n) (s : DAState n) : Prop

Run-state invariant for proposer optimality.

NoAchievableRejection w m s says: at state s, for every achievable pair (j, wj), if man j has already proposed to wj (i.e. idxOf wj < nextChoice j), then wj is currently holding j. Contrapositively, j has not been rejected by wj.

Equations

• GS.NoAchievableRejection w m s = ∀ (j wj : Fin n), GS.IsAchievable w m j wj → List.idxOf wj (m.prefs j) < s.nextChoice j → s.holding wj = some j

theorem GS.initState_NoAchievableRejection {n : ℕ} [NeZero n] (w m : Preferences n) : NoAchievableRejection w m (initState n)

The invariant holds vacuously at initState: no man has proposed yet.

theorem GS.daStep_NoAchievableRejection {n : ℕ} [NeZero n] (w m : Preferences n) (s : DAState n) (hhold : HoldInv m s) (hinj : ∀ (j1 j2 i : Fin n), s.holding j1 = some i → s.holding j2 = some i → j1 = j2) (hinv : NoAchievableRejection w m s) : NoAchievableRejection w m (daStep w m s)

Inductive step (KEY LEMMA). NoAchievableRejection is preserved by one daStep. Also threads HoldInv (for the old-holder index bound) and holding-injectivity (a man is held by at most one woman).

Proof: reduce (daStep).holding wj to its match and split on whether j had already proposed to wj before this round (hinv then pins s.holding wj = some j) or proposes exactly now (j ∈ pl wj). In every branch where some h ≠ j ends up holding wj, the local build_block helper produces a blocking pair (h, wj) for the achievability witness μ:

• wj prefers h to j = μ.matchM wj — because daStep's argmin/if chose h over j (and idxOf is injective on the Nodup list).
• h prefers wj to his μ-partner wh — because (m.prefs h).idxOf wj ≤ s.nextChoice h (propTarget identity if h just proposed; HoldInv if h was already holding wj), while hinv applied to (h, wh) forces s.nextChoice h ≤ (m.prefs h).idxOf wh (using that h is not held by wh at s — freshness, or injectivity since h holds wj ≠ wh).

A blocking pair contradicts μ's stability, so no such displacement occurs: wj keeps/takes j, and the invariant is preserved.

theorem GS.daRun_NoAchievableRejection {n : ℕ} [NeZero n] (w m : Preferences n) (fuel : ℕ) (s : DAState n) (hhold : HoldInv m s) (hinj : ∀ (j1 j2 i : Fin n), s.holding j1 = some i → s.holding j2 = some i → j1 = j2) (hinv : NoAchievableRejection w m s) : NoAchievableRejection w m (daRun w m fuel s)

NoAchievableRejection is preserved by daRun (threading HoldInv and holding-injectivity, both also preserved by daStep).

theorem GS.finalState_NoAchievableRejection {n : ℕ} [NeZero n] (w m : Preferences n) : NoAchievableRejection w m (finalState w m)

The invariant holds at finalState.

Main theorem

theorem GS.galeShapley_isProposingOptimal {n : ℕ} [NeZero n] (w m : Preferences n) (μ : Matching (Fin n) (Fin n)) (hμ : Matching.IsStable (MatchingMarket.ofEquivData w m) μ) (j wj : Fin n) : μ.matchW j = some wj → List.idxOf ((Equiv.ofBijective (gs w m) ⋯).symm j) (m.prefs j) ≤ List.idxOf wj (m.prefs j)

Men-optimal stable matching (Gale–Shapley 1962, [MSZ 22.10]): in the men-proposing DA, every man's GS partner is at least as preferred (by him) as his partner under any other stable matching μ.

Equivalently: for any stable μ pairing man j with woman wj, the GS output's matching of j is ranked at most as high (i.e., as good or better) as wj in m.prefs j.