EconCSLib.MarketDesign.Matching.Basic

Stable matching theory: two-sided markets where agents on each side have preferences over agents on the other side.

Main definitions

• MatchingMarket — a two-sided market with bundled preferences over partners
• Matching — a matching between two sets
• IsBlocking — a blocking pair [MSZ 22.5]
• IsStable — a stable matching (no blocking pair) [MSZ 22.5]
• IsIndividuallyRational — every matched agent strictly prefers their partner to being unmatched

Design

MatchingMarket stores only preference data. It does not bake [Fintype M] [Fintype W] into the structure. Finiteness belongs at the algorithm or existence-theorem layer, not in the market itself.

Preferences are bundled using the foundation-level Pref interface, applied to Option W and Option M so that none represents being unmatched. Strict preference is derived uniformly via strict.

References

• [MSZ] Chapter 22
• Gale, D. and Shapley, L.S. (1962). "College Admissions and the Stability of Marriage".

Matching market

structure MatchingMarket (M : Type u_1) (W : Type u_2) : Type (max u_1 u_2)

A two-sided matching market. M and W are the two sides (e.g., men and women, hospitals and residents). Each agent has a preference over agents on the other side plus the option of being unmatched (none).

• prefM : M → Pref (Option W)

  Each agent on side M has a preference over Option W.

• prefW : W → Pref (Option M)

  Each agent on side W has a preference over Option M.

Matching

structure Matching (M : Type u_1) (W : Type u_2) : Type (max u_1 u_2)

A matching is a partial bijection between M and W. matchM i is the partner of i ∈ M (or none if unmatched). matchW j is the partner of j ∈ W (or none if unmatched).

• matchM : M → Option W

  Partner of each agent on side M.

• matchW : W → Option M

  Partner of each agent on side W.

• consistent (m : M) (w : W) : self.matchM m = some w ↔ self.matchW w = some m

  Consistency: matchM m = some w ↔ matchW w = some m.

theorem Matching.ext_iff {M : Type u_1} {W : Type u_2} {x y : Matching M W} : x = y ↔ x.matchM = y.matchM ∧ x.matchW = y.matchW

theorem Matching.ext {M : Type u_1} {W : Type u_2} {x y : Matching M W} (matchM : x.matchM = y.matchM) (matchW : x.matchW = y.matchW) : x = y

Stability

def Matching.IsBlocking {M : Type u_1} {W : Type u_2} (market : MatchingMarket M W) (μ : Matching M W) (m : M) (w : W) : Prop

A pair (m, w) is a blocking pair for matching μ if both m and w strictly prefer each other to their current partners. [MSZ 22.5]

Equations

• Matching.IsBlocking market μ m w = (strict (market.prefM m).rel (some w) (μ.matchM m) ∧ strict (market.prefW w).rel (some m) (μ.matchW w))

def Matching.IsStable {M : Type u_1} {W : Type u_2} (market : MatchingMarket M W) (μ : Matching M W) : Prop

A matching is stable if it has no blocking pair. [MSZ 22.5]

Equations

• Matching.IsStable market μ = ∀ (m : M) (w : W), ¬Matching.IsBlocking market μ m w

def Matching.IsIndividuallyRational {M : Type u_1} {W : Type u_2} (market : MatchingMarket M W) (μ : Matching M W) : Prop

A matching is individually rational if every matched agent strictly prefers their partner to being unmatched.

Equations

• One or more equations did not get rendered due to their size.