College assignments, quotas and stability

Definition

AMLGS62Rest_AppliedModelingLib_Markets_Matching_ManyToOne

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

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

An assignment between applicants $A$ and colleges $C$ consists of an optional college $\mu(a)$ for each applicant and a finite roster $R_c$ for each college, with $\mu(a)=c$ if and only if $a\in R_c$ . Given quotas $q(c)$ and real values $u_a(c),v_c(a)$ , an unassigned applicant receives value zero. A college would accept an applicant if it has a vacant seat and values that applicant positively, or if it values the applicant above someone on its current roster. Stability requires quota feasibility, nonnegative values for assigned applicants and colleges, and no applicant–college pair where the applicant strictly improves and the college would accept. These definitions allow arbitrary quotas, unmatched applicants and unfilled seats.

Definition code

import Mathlib.Algebra.BigOperators.Ring.Finset
import Mathlib.Algebra.Order.BigOperators.Group.Finset
import Mathlib.Data.Finset.Basic
import Mathlib.Data.Finset.Card
import Mathlib.Data.Finset.Max
import Mathlib.Data.Fintype.Basic
import Mathlib.Data.Fintype.Card
import Mathlib.Data.Fintype.Perm
import Mathlib.Data.Fintype.Sigma
import Mathlib.Data.Real.Basic
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

namespace AppliedModelingLib
namespace Matching

/-- A many-to-one assignment between applicants and colleges. -/
structure ManyToOneAssignment (Applicants Colleges : Type*) where
  app_match : Applicants → Option Colleges
  college_roster : Colleges → Finset Applicants
  consistent : ∀ a c, app_match a = some c ↔ a ∈ college_roster c

namespace ManyToOneAssignment

/-- A many-to-one assignment respects college quotas. -/
def RespectsQuota {Applicants Colleges : Type*}
    (quota : Colleges → ℕ) (mu : ManyToOneAssignment Applicants Colleges) : Prop :=
  ∀ c, (mu.college_roster c).card ≤ quota c

end ManyToOneAssignment

namespace ManyToOne

/-- Applicant utility from an optional college assignment. -/
def valApplicant {Applicants Colleges : Type*}
    (val_applicant : Applicants → Colleges → ℝ)
    (a : Applicants) (c : Option Colleges) : ℝ :=
  match c with
  | none => 0
  | some c' => val_applicant a c'

/--
College `c` would accept applicant `a` relative to roster `s`: either `c` has a
free acceptable seat or `c` strictly prefers `a` to some currently assigned
applicant.
-/
def CollegeWouldAccept {Applicants Colleges : Type*}
    (val_college : Colleges → Applicants → ℝ)
    (quota : Colleges → ℕ) (s : Finset Applicants)
    (a : Applicants) (c : Colleges) : Prop :=
  (0 < val_college c a ∧ s.card < quota c) ∨
    ∃ a' ∈ s, val_college c a' < val_college c a

/-- Stability for many-to-one college-admissions/hospital-resident assignments. -/
def IsStable {Applicants Colleges : Type*}
    (val_applicant : Applicants → Colleges → ℝ)
    (val_college : Colleges → Applicants → ℝ)
    (quota : Colleges → ℕ)
    (mu : ManyToOneAssignment Applicants Colleges) : Prop :=
  ManyToOneAssignment.RespectsQuota quota mu ∧
    (∀ a, 0 ≤ valApplicant val_applicant a (mu.app_match a)) ∧
    (∀ c a, a ∈ mu.college_roster c → 0 ≤ val_college c a) ∧
    (∀ a c,
      valApplicant val_applicant a (mu.app_match a) < val_applicant a c →
        CollegeWouldAccept val_college quota (mu.college_roster c) a c →
          False)

end ManyToOne

end Matching
end AppliedModelingLib

Source

https://github.com/nikhgarg/AppliedModelingLib/blob/e952266be81e96bbeecea6af83d639af324a4438/AppliedModelingLib/Markets/Matching/ManyToOne.lean#L26-L295

View graph