Waiting-list stability and applicant-optimality statements

Definition

AMLGS62Rest_GS62CollegeAdmissions_PaperInterface

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

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

For finite applicant and college sets, arbitrary natural-number quotas, injective preference values within each participant's ranking, and no value equal to the outside option zero, define two propositions about the simultaneous waiting-list assignment $\mu^*$ . The Section 4 proposition says the procedure has no remaining active applicant and $\mu^*$ is quota-feasible, individually rational and free of blocking pairs. The Theorem 2 proposition says that for every stable assignment $\nu$ in the same market,

\forall a,\qquad U_a(\nu(a))\le U_a(\mu^*(a)).

Positive values encode acceptable list entries and negative values omitted entries. These transparent propositions are stated separately: the comparison proposition does not itself include a separate assertion of stability.

Definition code

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_Markets_Matching_ManyToOne
import Definitions.Def_AMLGS62Rest_GS62CollegeAdmissions_ExactCollegeBatchedProcedure

namespace GS62CollegeAdmissions
namespace PaperInterface

open AppliedModelingLib.Matching

/-- The Section 4 waiting-list procedure terminates in a stable assignment. -/
def section4_waiting_list_terminal_stabilitySpec : Prop :=
  ∀ {Applicants Colleges : Type*}
    [Fintype Applicants] [Fintype Colleges]
    [DecidableEq Applicants] [DecidableEq Colleges]
    (quota : Colleges → ℕ)
    (val_applicant : Applicants → Colleges → ℝ)
    (val_college : Colleges → Applicants → ℝ)
    (happlicant_strict :
      (∀ a c c', val_applicant a c = val_applicant a c' → c = c') ∧
        ∀ a c, val_applicant a c ≠ 0)
    (hcollege_strict :
      (∀ c a a', val_college c a = val_college c a' → a = a') ∧
        ∀ c a, val_college c a ≠ 0),
    (¬ ∃ a, ExactCollegeBatchedProcedure.SourceActive quota val_applicant
      val_college hcollege_strict.1
        (ExactCollegeBatchedProcedure.sourceWaitingListFinalState quota
          val_applicant val_college hcollege_strict.1 happlicant_strict.1) a) ∧
      ((∀ c,
          ((ExactCollegeBatchedProcedure.sourceWaitingListFinalAssignment quota
            val_applicant val_college hcollege_strict.1 happlicant_strict.1).college_roster c).card ≤ quota c) ∧
        (∀ a, 0 ≤ ManyToOne.valApplicant val_applicant a
          ((ExactCollegeBatchedProcedure.sourceWaitingListFinalAssignment quota
            val_applicant val_college hcollege_strict.1 happlicant_strict.1).app_match a)) ∧
        (∀ c a, a ∈
          (ExactCollegeBatchedProcedure.sourceWaitingListFinalAssignment quota
            val_applicant val_college hcollege_strict.1 happlicant_strict.1).college_roster c →
            0 ≤ val_college c a) ∧
        (∀ a c,
          ManyToOne.valApplicant val_applicant a
            ((ExactCollegeBatchedProcedure.sourceWaitingListFinalAssignment quota
              val_applicant val_college hcollege_strict.1 happlicant_strict.1).app_match a) <
            val_applicant a c →
          ((0 < val_college c a ∧
            ((ExactCollegeBatchedProcedure.sourceWaitingListFinalAssignment quota
              val_applicant val_college hcollege_strict.1 happlicant_strict.1).college_roster c).card < quota c) ∨
            ∃ a' ∈
              (ExactCollegeBatchedProcedure.sourceWaitingListFinalAssignment quota
                val_applicant val_college hcollege_strict.1 happlicant_strict.1).college_roster c,
              val_college c a' < val_college c a) →
            False))

/--
Theorem 2 under the completed operational stability reading of Sections 4--5.
The stable comparison class and applicant-wise conclusion are written out here,
rather than routed through a paper-local wrapper.  Section 4's separate
terminal-stability conclusion is not repeated as part of this theorem target.
-/
def theorem2_applicant_optimalitySpec : Prop :=
  ∀ {Applicants Colleges : Type*}
    [Fintype Applicants] [Fintype Colleges]
    [DecidableEq Applicants] [DecidableEq Colleges]
    (quota : Colleges → ℕ)
    (val_applicant : Applicants → Colleges → ℝ)
    (val_college : Colleges → Applicants → ℝ)
    (happlicant_strict :
      (∀ a c c', val_applicant a c = val_applicant a c' → c = c') ∧
        ∀ a c, val_applicant a c ≠ 0)
    (hcollege_strict :
      (∀ c a a', val_college c a = val_college c a' → a = a') ∧
        ∀ c a, val_college c a ≠ 0),
    ∀ (nu : ManyToOneAssignment Applicants Colleges),
      ((∀ c, (nu.college_roster c).card ≤ quota c) ∧
        (∀ a, 0 ≤ ManyToOne.valApplicant val_applicant a (nu.app_match a)) ∧
        (∀ c a, a ∈ nu.college_roster c → 0 ≤ val_college c a) ∧
        (∀ a c,
          ManyToOne.valApplicant val_applicant a (nu.app_match a) <
            val_applicant a c →
          ((0 < val_college c a ∧ (nu.college_roster c).card < quota c) ∨
            ∃ a' ∈ nu.college_roster c,
              val_college c a' < val_college c a) →
            False)) →
        ∀ a,
          ManyToOne.valApplicant val_applicant a (nu.app_match a) ≤
            ManyToOne.valApplicant val_applicant a
              ((ExactCollegeBatchedProcedure.sourceWaitingListFinalAssignment quota
                val_applicant val_college hcollege_strict.1 happlicant_strict.1).app_match a)

end PaperInterface
end GS62CollegeAdmissions

Source

https://github.com/nikhgarg/AppliedModelingLib/blob/e952266be81e96bbeecea6af83d639af324a4438/papers/GS62CollegeAdmissions/PaperInterface.lean#L97-L173

View graph