Rural hospitals theorem, one-position case: unmatched doctors
ProvedRuralHospitals.one_to_one_unmatched_doctorConsider 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 doctor ,
This is the doctor half of Part 1 of the rural hospitals theorem in the special case of one position per hospital (the stable marriage setting with unequal sides), first proved by McVitie and 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_doctor {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 ν) (d : D) (hd : μ d = none) :
ν d = none := by sorry
end RuralHospitals
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.