Market Design.Matching.One To One

9 nodes 4 formalized 4 proved 1 staged

Market-Design Matching: One-to-One Topic Catalog

Canonical folder topic: market_design.matching.one_to_one

Scope

One-to-one stable matching (marriage market) per Gale-Shapley 1962 and Roth-Sotomayor 1990. Covers the core data structures (matching market, matching, stability) and the four central theorems: Gale-Shapley existence, proposing-side optimality, lattice structure of stable matchings, and Roth 1982 strategy-proofness for the proposing side.

Many-to-one (college admission), housing markets (TTC), and assignment games (Demange-Gale-Sotomayor) live under sibling subtopics market_design.matching.{many_to_one,housing,assignment}.

References

[MSZ Ch.22, §22.1–22.4] Maschler, Solan, Zamir, Game Theory.. Primary source for definitions, theorems, and proofs of GS existence, lattice, and Rural Hospitals.
Gale & Shapley (1962). College Admissions and the Stability of Marriage. AMM 69, 9–15.
Roth (1982). The Economics of Matching: Stability and Incentives. Math. Oper. Res. 7, 617–628.
Roth & Sotomayor (1990). Two-Sided Matching. Cambridge UP.

Definition Gale-Shapley Deferred Acceptance Algorithm formalized

Theorem Gale-Shapley Theorem (Existence of Stable Matching) proved

Theorem Lattice Structure of Stable Matchings (Conway-Knuth) proved

Definition Matching (Partial Bijection) formalized

Definition Matching Market (One-to-One) formalized

Theorem Proposing-Side Optimal Stable Matching proved

Theorem Rural Hospitals Theorem proved

Definition Stability (Individual Rationality + No Blocking Pair) formalized

Theorem Strategy-Proofness of Gale-Shapley for the Proposing Side (Roth 1982) staged