Rural hospitals theorem, one-position case: unmatched hospitals
ProvedRuralHospitals.one_to_one_unmatched_hospitalConsider a matching market with a finite set of doctors and a finite set of hospitals, in which every hospital has exactly one position and all preferences are strict. Let and be two stable matchings. For every hospital ,
where denotes the set of doctors assigned to in . In words: a hospital unmatched in one stable matching is unmatched in every stable matching.
This is the hospital half of Part 1 of the rural hospitals theorem in the one-position special case (McVitie–Wilson 1970).
Formalization Note Uses the model RuralHospitals.Market (definition RuralHospitals_Market): finite types D (doctors) and H (hospitals); strict preferences given by injective rank functions on Option H / Option D (smaller rank = preferred, none = unmatched / empty position); responsive hospital preferences; capacities capacity : H → ℕ. An assignment is a map μ : D → Option H, and assigned μ h is the finite set of doctors placed at h.
import Mathlib import Definitions.Def_RuralHospitals_Market
namespace RuralHospitals
theorem one_to_one_unmatched_hospital {D H : Type*} [Fintype D] [Fintype H] [DecidableEq H]
(M : Market D H) (hcap : ∀ h, M.capacity h = 1) (μ ν : Assignment D H)
(hμ : M.IsStable μ) (hν : M.IsStable ν) (h : H) (hh : assigned μ h = ∅) :
assigned ν h = ∅ := by sorry
end RuralHospitals
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.