EconCSLib.MarketDesign.Matching.RuralHospitals #

Rural Hospitals theorem, specialized to the balanced full-preference one-to-one market (Preferences n via MatchingMarket.ofEquivData).

In that model every agent is acceptable to every other and |M| = |W| = n, so the general statement ("the set of matched participants is the same in every stable matching") collapses to: every stable matching is perfect — all n women and all n men are matched. Hence the matched set is the whole of Fin n in every stable matching, trivially invariant across them.

Main result #

GS.stable_matching_perfect — every stable matching on MatchingMarket.ofEquivData w m matches every agent on both sides.

Proof #

If some woman were unmatched, then matchW (men → women) cannot be total: were it total it would be an injection Fin n → Fin n, hence a bijection, forcing the unmatched woman to be someone's partner. So some man is also unmatched — and an unmatched woman together with an unmatched man form a blocking pair (each strictly prefers any partner to staying single, since none is the least-preferred option), contradicting stability. The man side is symmetric, using totality of matchM.

References #

[MSZ Theorem 22.14] Maschler, Solan, Zamir, Game Theory, §22.
Roth (1986); McVitie–Wilson (1970).

source

theorem GS.stable_matching_perfect {n : ℕ} (w m : Preferences n) (μ : Matching (Fin n) (Fin n)) (hμ : Matching.IsStable (MatchingMarket.ofEquivData w m) μ) :

(∀ (i : Fin n), (μ.matchM i).isSome = true) ∧ ∀ (j : Fin n), (μ.matchW j).isSome = true

In the balanced full-preference one-to-one market, every stable matching is perfect: every woman and every man is matched. This is the Rural-Hospitals specialization — the matched set is all of Fin n in every stable matching, hence invariant across the stable set.