A terminal state with impossible rejections is applicant-optimal

Proved

GS62CollegeAdmissions.ExactCollegeBatchedProcedure.sourceAssignmentFromState_applicant_optimal_of_terminated_rejections

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

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

Let applicants $A$ and colleges $C$ be finite with decidable equality, quotas $q:C\to\mathbb N$ , and real values that are injective within each participant's ranking and never zero. A pair is eligible when both values are positive. In a state of accumulated applications $H_c$ , college $c$ retains its best quota-many applicants. Suppose its waiting lists are disjoint, every application is eligible, and each applicant weakly prefers every previously tried college to every still-untried eligible college. Suppose no unassigned applicant has an untried eligible college. Finally, suppose that if $a\in H_c$ but $a$ is not retained by $c$ , no stable assignment matches $a$ to $c$ .

The assignment $\mu$ formed from these waiting lists is stable, and

\forall\nu\text{ stable},\quad\forall a,\qquad U_a(\nu(a))\le U_a(\mu(a)).

Here stability includes quotas, individual rationality and absence of replacement or vacancy blocks, and $U_a(\bot)=0$ . The state need only satisfy the stated conditions; it need not be supplied with an algorithmic history.

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 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.ExactCollegeBatchedProcedure

open AppliedModelingLib.Matching
open AppliedModelingLib.FiniteChoice

variable {Applicants Colleges : Type*}
  [Fintype Applicants] [Fintype Colleges]
  [DecidableEq Applicants] [DecidableEq Colleges]

Formal statement

theorem GS62CollegeAdmissions.ExactCollegeBatchedProcedure.sourceAssignmentFromState_applicant_optimal_of_terminated_rejections
    (quota : Colleges -> Nat)
    (val_applicant : Applicants -> Colleges -> Real)
    (val_college : Colleges -> Applicants -> Real)
    (hdomain : gs_strict_college_admissions_domain
      val_applicant val_college)
    (s : SourceWaitingListState Applicants Colleges)
    (hinv : SourceStateInvariant quota val_applicant val_college
      hdomain.2.1 s)
    (hterm : ¬ (exists a, SourceActive quota val_applicant val_college
      hdomain.2.1 s a))
    (hrejected : SourceRejectedPairImpossible quota val_applicant val_college
      hdomain.2.1 s) :
    gs_applicant_optimal_college_assignment quota val_applicant val_college
      (sourceAssignmentFromState quota val_applicant val_college
        hdomain.2.1 s hinv) := by sorry

Source

https://github.com/nikhgarg/AppliedModelingLib/blob/e952266be81e96bbeecea6af83d639af324a4438/papers/GS62CollegeAdmissions/ExactCollegeBatchedProcedure.lean#L1401-L1468

View graph