Gale–Shapley Section 4: waiting lists terminate in a stable assignment

Proved

GS62CollegeAdmissions.PaperInterface.section4_waiting_list_terminal_stability

by nkgarg · Sep 15, 2026 · Mathlib c5ea003 (Lean v4.30.0)

aml-gs62-stable-marriage-20260915college-admissionsgame-theorystable-matching

Let $A,C$ be finite sets with decidable equality, let each college have an arbitrary quota $q(c)\in\mathbb N$ , and let applicant and college values be real, injective across each participant's potential partners, and nonzero. Zero is the outside option, so positive values encode acceptable partners and negative values omitted partners. Starting with no applications, every unassigned applicant with an untried mutually acceptable college simultaneously applies to the highest-ranked such college, and each college keeps its best applicants up to its quota.

The recursively defined terminal state has no active applicant. Its assignment $\mu^*$ respects every quota, gives nonnegative value to assigned participants, and has no applicant–college pair where the applicant strictly improves and the college either fills an acceptable vacancy or replaces a less-preferred assignee. Empty sets, zero quotas and incomplete acceptable lists are included.

Preamble

import Mathlib.Algebra.BigOperators.Ring.Finset
import Mathlib.Algebra.Order.BigOperators.Group.Finset
import Mathlib.Data.Fin.VecNotation
import Mathlib.Data.Finset.Basic
import Mathlib.Data.Finset.Card
import Mathlib.Data.Finset.Lattice.Basic
import Mathlib.Data.Finset.Max
import Mathlib.Data.Finset.Sort
import Mathlib.Data.Fintype.Basic
import Mathlib.Data.Fintype.Card
import Mathlib.Data.Fintype.EquivFin
import Mathlib.Data.Fintype.Option
import Mathlib.Data.Fintype.Perm
import Mathlib.Data.Fintype.Sigma
import Mathlib.Data.Fintype.Sort
import Mathlib.Data.Prod.Lex
import Mathlib.Data.Real.Basic
import Mathlib.Tactic
import Mathlib.Tactic.FinCases
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Ring
import Definitions.Def_AMLGS62_AppliedModelingLib_Markets_Matching_Basic
import Definitions.Def_AMLGS62_AppliedModelingLib_Markets_Matching_DeferredAcceptance
import Definitions.Def_AMLGS62_AppliedModelingLib_Markets_Matching_ManyToOne
import Definitions.Def_AMLGS62_GS62CollegeAdmissions_MainTheorems
import Definitions.Def_AMLGS62Rest_AppliedModelingLib_Foundations_Math_FiniteChoice
import Definitions.Def_AMLGS62Rest_AppliedModelingLib_Markets_Matching_ManyToOne
import Definitions.Def_AMLGS62Rest_GS62CollegeAdmissions_ExactCollegeBatchedProcedure
import Definitions.Def_AMLGS62Rest_GS62CollegeAdmissions_PaperInterface
import Definitions.Def_AMLGS62Rest_GS62CollegeAdmissions_SourceCompletion
import Definitions.Def_AMLGS62Rest_GS62CollegeAdmissions_SourceModel

open GS62CollegeAdmissions
open GS62CollegeAdmissions.PaperInterface

open AppliedModelingLib.Matching

Formal statement

theorem GS62CollegeAdmissions.PaperInterface.section4_waiting_list_terminal_stability :
    section4_waiting_list_terminal_stabilitySpec := by sorry

Source

https://github.com/nikhgarg/AppliedModelingLib/blob/e952266be81e96bbeecea6af83d639af324a4438/papers/GS62CollegeAdmissions/ProofInterface.lean#L62-L78

View graph