Simultaneous college waiting lists and their terminal assignment

Definition
AMLGS62Rest_GS62CollegeAdmissions_ExactCollegeBatchedProcedure
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, a state records each college's accumulated applications $H_c$ . College $c$ retains the highest-valued $\min(q(c),|H_c|)$ applicants as its waiting list. A pair is eligible when both values are positive. An active applicant belongs to no waiting list and has an eligible college not yet applied to. In one round every active applicant applies to a highest-valued untried eligible college; colleges accumulate the new applications and update their waiting lists. Starting from empty histories, the procedure recurses until no applicant is active, using the finite count of untried eligible pairs as a decreasing measure.
The state invariant requires disjoint waiting lists, eligibility of every recorded application, and preference for every previously tried college over any still-untried eligible college. It permits construction of a consistent assignment from the waiting lists. A rejected pair is impossible when no stable assignment matches an applicant to a college that has received but does not retain that applicant. The bundle defines the procedure, invariant, rejection property and terminal assignment and retains the existing proofs needed to define them.
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 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

namespace GS62CollegeAdmissions
namespace ExactCollegeBatchedProcedure

open AppliedModelingLib.Matching
open AppliedModelingLib.FiniteChoice

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

/-- A pair may occur in the source procedure exactly when both sides list it. -/
def sourceEligible
    (val_applicant : Applicants -> Colleges -> Real)
    (val_college : Colleges -> Applicants -> Real)
    (a : Applicants) (c : Colleges) : Prop :=
  0 < val_applicant a c /\ 0 < val_college c a

/-- Higher college scores occur first in the induced applicant order. -/
@[reducible] noncomputable def collegeOrder
    (val_college : Colleges -> Applicants -> Real)
    (hcollegeStrict : forall c a a',
      val_college c a = val_college c a' -> a = a')
    (c : Colleges) : LinearOrder Applicants :=
  LinearOrder.lift' (α := Applicants) (β := OrderDual Real)
    (fun a => OrderDual.toDual (val_college c a))
    (by
      intro a b h
      exact hcollegeStrict c a b h)

/-- The literal top-`q` waiting-list selection at one college. -/
noncomputable def collegeTopQ
    (quota : Colleges -> Nat)
    (val_college : Colleges -> Applicants -> Real)
    (hcollegeStrict : forall c a a',
      val_college c a = val_college c a' -> a = a')
    (c : Colleges) (pool : Finset Applicants) : Finset Applicants :=
  letI : LinearOrder Applicants := collegeOrder val_college hcollegeStrict c
  linearTopQChoice (quota c) pool

theorem collegeTopQ_subset
    (quota : Colleges -> Nat)
    (val_college : Colleges -> Applicants -> Real)
    (hcollegeStrict : forall c a a',
      val_college c a = val_college c a' -> a = a')
    (c : Colleges) (pool : Finset Applicants) :
    collegeTopQ quota val_college hcollegeStrict c pool <= pool := by
  classical
  letI : LinearOrder Applicants := collegeOrder val_college hcollegeStrict c
  exact linearTopQChoice_feasible (α := Applicants) (quota c) pool

 theorem collegeTopQ_substitutable
    (quota : Colleges -> Nat)
    (val_college : Colleges -> Applicants -> Real)
    (hcollegeStrict : forall c a a',
      val_college c a = val_college c a' -> a = a')
    (c : Colleges) :
    Substitutable (collegeTopQ quota val_college hcollegeStrict c) := by
  classical
  letI : LinearOrder Applicants := collegeOrder val_college hcollegeStrict c
  unfold collegeTopQ
  have hsub : Substitutable (linearTopQChoice (α := Applicants) (quota c)) :=
    substitutable_of_feasible_of_qRepresentative
    (C := linearTopQChoice (α := Applicants) (quota c))
    (q := quota c)
    (linearTopQChoice_feasible (α := Applicants) (quota c))
    (linearTopQChoice_qRepresentative (α := Applicants) (quota c))
  intro X1 X2 hsubset x hx
  exact hsub hsubset hx

/-- Direct source state: cumulative applications received by every college. -/
structure SourceWaitingListState (Applicants Colleges : Type*)
    [DecidableEq Applicants] where
  applications : Colleges -> Finset Applicants

/-- A college's current waiting list is the top quota-many applications seen. -/
noncomputable def waitingList
    (quota : Colleges -> Nat)
    (val_college : Colleges -> Applicants -> Real)
    (hcollegeStrict : forall c a a',
      val_college c a = val_college c a' -> a = a')
    (s : SourceWaitingListState Applicants Colleges) (c : Colleges) :
    Finset Applicants :=
  collegeTopQ quota val_college hcollegeStrict c (s.applications c)

/-- The source states reachable from the empty application history. -/
def SourceStateInvariant
    (quota : Colleges -> Nat)
    (val_applicant : Applicants -> Colleges -> Real)
    (val_college : Colleges -> Applicants -> Real)
    (hcollegeStrict : forall c a a',
      val_college c a = val_college c a' -> a = a')
    (s : SourceWaitingListState Applicants Colleges) : Prop :=
  (forall a c d,
      a ∈ waitingList quota val_college hcollegeStrict s c ->
      a ∈ waitingList quota val_college hcollegeStrict s d -> c = d) /\
    (forall a c, a ∈ s.applications c ->
      sourceEligible val_applicant val_college a c) /\
    forall a c d, a ∈ s.applications c ->
      sourceEligible val_applicant val_college a d ->
      a ∉ s.applications d ->
      val_applicant a d <= val_applicant a c

/-- The unique college whose waiting list currently contains an applicant. -/
noncomputable def assignedCollege
    (quota : Colleges -> Nat)
    (val_college : Colleges -> Applicants -> Real)
    (hcollegeStrict : forall c a a',
      val_college c a = val_college c a' -> a = a')
    (s : SourceWaitingListState Applicants Colleges) (a : Applicants) :
    Option Colleges := by
  classical
  exact if h : exists c,
      a ∈ waitingList quota val_college hcollegeStrict s c then
    some (Classical.choose h)
  else none

theorem assignedCollege_eq_some_iff
    (quota : Colleges -> Nat)
    (val_applicant : Applicants -> Colleges -> Real)
    (val_college : Colleges -> Applicants -> Real)
    (hcollegeStrict : forall c a a',
      val_college c a = val_college c a' -> a = a')
    (s : SourceWaitingListState Applicants Colleges)
    (hinv : SourceStateInvariant quota val_applicant val_college
      hcollegeStrict s)
    (a : Applicants) (c : Colleges) :
    assignedCollege quota val_college hcollegeStrict s a = some c <->
      a ∈ waitingList quota val_college hcollegeStrict s c := by
  classical
  unfold assignedCollege
  by_cases h : exists d,
      a ∈ waitingList quota val_college hcollegeStrict s d
  · rw [dif_pos h]
    constructor
    · intro heq
      have hc : Classical.choose h = c := Option.some.inj heq
      simpa [hc] using Classical.choose_spec h
    · intro hac
      have hc : Classical.choose h = c :=
        hinv.1 a (Classical.choose h) c (Classical.choose_spec h) hac
      simp [hc]
  · rw [dif_neg h]
    constructor
    · intro hnone
      cases hnone
    · intro hac
      exact False.elim (h ⟨c, hac⟩)

/-- Mutually acceptable colleges to which this applicant has not yet applied. -/
noncomputable def untriedEligibleColleges
    (val_applicant : Applicants -> Colleges -> Real)
    (val_college : Colleges -> Applicants -> Real)
    (s : SourceWaitingListState Applicants Colleges) (a : Applicants) :
    Finset Colleges := by
  classical
  exact Finset.univ.filter fun c =>
    sourceEligible val_applicant val_college a c /\ a ∉ s.applications c

/-- An applicant acts in a round iff unmatched and an eligible target remains. -/
def SourceActive
    (quota : Colleges -> Nat)
    (val_applicant : Applicants -> Colleges -> Real)
    (val_college : Colleges -> Applicants -> Real)
    (hcollegeStrict : forall c a a',
      val_college c a = val_college c a' -> a = a')
    (s : SourceWaitingListState Applicants Colleges) (a : Applicants) : Prop :=
  assignedCollege quota val_college hcollegeStrict s a = none /\
    (untriedEligibleColleges val_applicant val_college s a).Nonempty

 theorem exists_best_untried
    (val_applicant : Applicants -> Colleges -> Real)
    (val_college : Colleges -> Applicants -> Real)
    (s : SourceWaitingListState Applicants Colleges) (a : Applicants)
    (h : (untriedEligibleColleges val_applicant val_college s a).Nonempty) :
    exists c,
      c ∈ untriedEligibleColleges val_applicant val_college s a /\
        forall d, d ∈ untriedEligibleColleges val_applicant val_college s a ->
          val_applicant a d <= val_applicant a c := by
  exact Finset.exists_max_image _ _ h

/-- Best currently available source-level application target. -/
noncomputable def nextCollege
    (quota : Colleges -> Nat)
    (val_applicant : Applicants -> Colleges -> Real)
    (val_college : Colleges -> Applicants -> Real)
    (hcollegeStrict : forall c a a',
      val_college c a = val_college c a' -> a = a')
    (s : SourceWaitingListState Applicants Colleges) (a : Applicants) :
    Option Colleges := by
  classical
  if hactive : SourceActive quota val_applicant val_college
      hcollegeStrict s a then
    exact some (Classical.choose
      (exists_best_untried val_applicant val_college s a hactive.2))
  else exact none

theorem nextCollege_eq_some_of_active
    (quota : Colleges -> Nat)
    (val_applicant : Applicants -> Colleges -> Real)
    (val_college : Colleges -> Applicants -> Real)
    (hcollegeStrict : forall c a a',
      val_college c a = val_college c a' -> a = a')
    (s : SourceWaitingListState Applicants Colleges) (a : Applicants)
    (hactive : SourceActive quota val_applicant val_college
      hcollegeStrict s a) :
    exists c,
      nextCollege quota val_applicant val_college hcollegeStrict s a = some c /\
      c ∈ untriedEligibleColleges val_applicant val_college s a /\
      forall d, d ∈ untriedEligibleColleges val_applicant val_college s a ->
        val_applicant a d <= val_applicant a c := by
  classical
  let hexists := exists_best_untried val_applicant val_college s a hactive.2
  let c := Classical.choose hexists
  have hspec := Classical.choose_spec hexists
  refine ⟨c, ?_, hspec.1, hspec.2⟩
  simp [nextCollege, hactive, c, hexists]

theorem nextCollege_eq_none_of_not_active
    (quota : Colleges -> Nat)
    (val_applicant : Applicants -> Colleges -> Real)
    (val_college : Colleges -> Applicants -> Real)
    (hcollegeStrict : forall c a a',
      val_college c a = val_college c a' -> a = a')
    (s : SourceWaitingListState Applicants Colleges) (a : Applicants)
    (hnot : ¬ SourceActive quota val_applicant val_college
      hcollegeStrict s a) :
    nextCollege quota val_applicant val_college hcollegeStrict s a = none := by
  simp [nextCollege, hnot]

/-- New applications received by one college in the current source round. -/
noncomputable def newApplications
    (quota : Colleges -> Nat)
    (val_applicant : Applicants -> Colleges -> Real)
    (val_college : Colleges -> Applicants -> Real)
    (hcollegeStrict : forall c a a',
      val_college c a = val_college c a' -> a = a')
    (s : SourceWaitingListState Applicants Colleges) (c : Colleges) :
    Finset Applicants := by
  classical
  exact Finset.univ.filter fun a =>
    nextCollege quota val_applicant val_college hcollegeStrict s a = some c

/-- One literal source round: add every unmatched applicant's next application. -/
noncomputable def sourceStep
    (quota : Colleges -> Nat)
    (val_applicant : Applicants -> Colleges -> Real)
    (val_college : Colleges -> Applicants -> Real)
    (hcollegeStrict : forall c a a',
      val_college c a = val_college c a' -> a = a')
    (s : SourceWaitingListState Applicants Colleges) :
    SourceWaitingListState Applicants Colleges where
  applications c := s.applications c ∪
    newApplications quota val_applicant val_college hcollegeStrict s c

theorem sourceActive_of_nextCollege_eq_some
    (quota : Colleges -> Nat)
    (val_applicant : Applicants -> Colleges -> Real)
    (val_college : Colleges -> Applicants -> Real)
    (hcollegeStrict : forall c a a',
      val_college c a = val_college c a' -> a = a')
    (s : SourceWaitingListState Applicants Colleges) (a : Applicants)
    {c : Colleges}
    (hnext : nextCollege quota val_applicant val_college
      hcollegeStrict s a = some c) :
    SourceActive quota val_applicant val_college hcollegeStrict s a := by
  by_contra hnot
  have hnone := nextCollege_eq_none_of_not_active
    quota val_applicant val_college hcollegeStrict s a hnot
  rw [hnone] at hnext
  cases hnext

theorem mem_newApplications_iff
    (quota : Colleges -> Nat)
    (val_applicant : Applicants -> Colleges -> Real)
    (val_college : Colleges -> Applicants -> Real)
    (hcollegeStrict : forall c a a',
      val_college c a = val_college c a' -> a = a')
    (s : SourceWaitingListState Applicants Colleges)
    (a : Applicants) (c : Colleges) :
    a ∈ newApplications quota val_applicant val_college hcollegeStrict s c <->
      nextCollege quota val_applicant val_college hcollegeStrict s a = some c := by
  classical
  simp [newApplications]

theorem mem_newApplications_spec
    (quota : Colleges -> Nat)
    (val_applicant : Applicants -> Colleges -> Real)
    (val_college : Colleges -> Applicants -> Real)
    (hcollegeStrict : forall c a a',
      val_college c a = val_college c a' -> a = a')
    (s : SourceWaitingListState Applicants Colleges)
    {a : Applicants} {c : Colleges}
    (hnew : a ∈ newApplications quota val_applicant val_college
      hcollegeStrict s c) :
    SourceActive quota val_applicant val_college hcollegeStrict s a /\
      c ∈ untriedEligibleColleges val_applicant val_college s a /\
      forall d, d ∈ untriedEligibleColleges val_applicant val_college s a ->
        val_applicant a d <= val_applicant a c := by
  have hnext := (mem_newApplications_iff quota val_applicant val_college
    hcollegeStrict s a c).1 hnew
  have hactive := sourceActive_of_nextCollege_eq_some
    quota val_applicant val_college hcollegeStrict s a hnext
  rcases nextCollege_eq_some_of_active quota val_applicant val_college
      hcollegeStrict s a hactive with ⟨c', hc', hmem, hbest⟩
  have hcc : c' = c := Option.some.inj (hc'.symm.trans hnext)
  subst c'
  exact ⟨hactive, hmem, hbest⟩

/-- No chosen applicant is newly created except at the college applied to. -/
theorem waitingList_sourceStep_subset_old_union_new
    (quota : Colleges -> Nat)
    (val_applicant : Applicants -> Colleges -> Real)
    (val_college : Colleges -> Applicants -> Real)
    (hcollegeStrict : forall c a a',
      val_college c a = val_college c a' -> a = a')
    (s : SourceWaitingListState Applicants Colleges) (c : Colleges) :
    waitingList quota val_college hcollegeStrict
        (sourceStep quota val_applicant val_college hcollegeStrict s) c <=
      waitingList quota val_college hcollegeStrict s c ∪
        newApplications quota val_applicant val_college hcollegeStrict s c := by
  classical
  intro a ha
  have haPool : a ∈ s.applications c ∪
      newApplications quota val_applicant val_college hcollegeStrict s c := by
    exact collegeTopQ_subset quota val_college hcollegeStrict c _
      (by simpa [waitingList, sourceStep] using ha)
  rcases Finset.mem_union.mp haPool with haOld | haNew
  · apply Finset.mem_union_left
    have hsub : Substitutable
        (collegeTopQ quota val_college hcollegeStrict c) :=
      collegeTopQ_substitutable quota val_college hcollegeStrict c
    exact hsub (X₁ := s.applications c)
      (X₂ := s.applications c ∪
        newApplications quota val_applicant val_college hcollegeStrict s c)
      Finset.subset_union_left
      (Finset.mem_inter.mpr ⟨haOld, by simpa [waitingList, sourceStep] using ha⟩)
  · exact Finset.mem_union_right _ haNew

theorem sourceStep_preserves_invariant
    (quota : Colleges -> Nat)
    (val_applicant : Applicants -> Colleges -> Real)
    (val_college : Colleges -> Applicants -> Real)
    (hcollegeStrict : forall c a a',
      val_college c a = val_college c a' -> a = a')
    (s : SourceWaitingListState Applicants Colleges)
    (hinv : SourceStateInvariant quota val_applicant val_college
      hcollegeStrict s) :
    SourceStateInvariant quota val_applicant val_college hcollegeStrict
      (sourceStep quota val_applicant val_college hcollegeStrict s) := by
  classical
  refine ⟨?_, ?_, ?_⟩
  · intro a c d hac had
    have hac' := waitingList_sourceStep_subset_old_union_new
      quota val_applicant val_college hcollegeStrict s c hac
    have had' := waitingList_sourceStep_subset_old_union_new
      quota val_applicant val_college hcollegeStrict s d had
    rcases Finset.mem_union.mp hac' with hacOld | hacNew
    · rcases Finset.mem_union.mp had' with hadOld | hadNew
      · exact hinv.1 a c d hacOld hadOld
      · have hactive := (mem_newApplications_spec quota val_applicant
          val_college hcollegeStrict s hadNew).1
        have hassigned := (assignedCollege_eq_some_iff quota val_applicant
          val_college hcollegeStrict s hinv a c).2 hacOld
        rw [hactive.1] at hassigned
        cases hassigned
    · rcases Finset.mem_union.mp had' with hadOld | hadNew
      · have hactive := (mem_newApplications_spec quota val_applicant
          val_college hcollegeStrict s hacNew).1
        have hassigned := (assignedCollege_eq_some_iff quota val_applicant
          val_college hcollegeStrict s hinv a d).2 hadOld
        rw [hactive.1] at hassigned
        cases hassigned
      · have hcNext := (mem_newApplications_iff quota val_applicant
          val_college hcollegeStrict s a c).1 hacNew
        have hdNext := (mem_newApplications_iff quota val_applicant
          val_college hcollegeStrict s a d).1 hadNew
        exact Option.some.inj (hcNext.symm.trans hdNext)
  · intro a c hac
    rcases Finset.mem_union.mp (by simpa [sourceStep] using hac) with
      hacOld | hacNew
    · exact hinv.2.1 a c hacOld
    · have hmem := (mem_newApplications_spec quota val_applicant
        val_college hcollegeStrict s hacNew).2.1
      exact (Finset.mem_filter.mp hmem).2.1
  · intro a c d hac hdEligible hdNot
    have hdNotOld : a ∉ s.applications d := by
      intro hdOld
      apply hdNot
      simp [sourceStep, hdOld]
    rcases Finset.mem_union.mp (by simpa [sourceStep] using hac) with
      hacOld | hacNew
    · exact hinv.2.2 a c d hacOld hdEligible hdNotOld
    · have hspec := mem_newApplications_spec quota val_applicant
        val_college hcollegeStrict s hacNew
      have hdMem : d ∈ untriedEligibleColleges
          val_applicant val_college s a := by
        simp [untriedEligibleColleges, hdEligible, hdNotOld]
      exact hspec.2.2 d hdMem

/-- Empty source application history. -/
def initialSourceState : SourceWaitingListState Applicants Colleges where
  applications _ := ∅

theorem initialSourceState_invariant
    (quota : Colleges -> Nat)
    (val_applicant : Applicants -> Colleges -> Real)
    (val_college : Colleges -> Applicants -> Real)
    (hcollegeStrict : forall c a a',
      val_college c a = val_college c a' -> a = a') :
    SourceStateInvariant quota val_applicant val_college hcollegeStrict
      (initialSourceState (Applicants := Applicants) (Colleges := Colleges)) := by
  classical
  refine ⟨?_, ?_, ?_⟩
  · intro a c d hac
    have hfalse : a ∈ (∅ : Finset Applicants) :=
      collegeTopQ_subset quota val_college hcollegeStrict c ∅
        (by simpa [waitingList, initialSourceState] using hac)
    simp at hfalse
  · simp [initialSourceState]
  · simp [initialSourceState]

/-- The finite measure of eligible applicant-college pairs not yet tried. -/
noncomputable def untriedEligiblePairs
    (val_applicant : Applicants -> Colleges -> Real)
    (val_college : Colleges -> Applicants -> Real)
    (s : SourceWaitingListState Applicants Colleges) :
    Finset (Applicants × Colleges) := by
  classical
  exact Finset.univ.filter fun p =>
    sourceEligible val_applicant val_college p.1 p.2 /\
      p.1 ∉ s.applications p.2

theorem mem_untriedEligiblePairs_iff
    (val_applicant : Applicants -> Colleges -> Real)
    (val_college : Colleges -> Applicants -> Real)
    (s : SourceWaitingListState Applicants Colleges)
    (a : Applicants) (c : Colleges) :
    (a, c) ∈ untriedEligiblePairs val_applicant val_college s <->
      c ∈ untriedEligibleColleges val_applicant val_college s a := by
  classical
  simp [untriedEligiblePairs, untriedEligibleColleges]

theorem untriedEligiblePairs_sourceStep_subset
    (quota : Colleges -> Nat)
    (val_applicant : Applicants -> Colleges -> Real)
    (val_college : Colleges -> Applicants -> Real)
    (hcollegeStrict : forall c a a',
      val_college c a = val_college c a' -> a = a')
    (s : SourceWaitingListState Applicants Colleges) :
    untriedEligiblePairs val_applicant val_college
        (sourceStep quota val_applicant val_college hcollegeStrict s) <=
      untriedEligiblePairs val_applicant val_college s := by
  classical
  intro p hp
  rcases Finset.mem_filter.mp hp with ⟨_hpUniv, hpEligible, hpNot⟩
  apply Finset.mem_filter.mpr
  refine ⟨Finset.mem_univ p, hpEligible, ?_⟩
  intro hpOld
  apply hpNot
  simp [sourceStep, hpOld]

theorem untriedEligiblePairs_sourceStep_ssubset_of_active
    (quota : Colleges -> Nat)
    (val_applicant : Applicants -> Colleges -> Real)
    (val_college : Colleges -> Applicants -> Real)
    (hcollegeStrict : forall c a a',
      val_college c a = val_college c a' -> a = a')
    (s : SourceWaitingListState Applicants Colleges)
    (hactive : exists a, SourceActive quota val_applicant val_college
      hcollegeStrict s a) :
    untriedEligiblePairs val_applicant val_college
        (sourceStep quota val_applicant val_college hcollegeStrict s) <
      untriedEligiblePairs val_applicant val_college s := by
  classical
  refine Finset.ssubset_iff_subset_ne.mpr
    ⟨untriedEligiblePairs_sourceStep_subset quota val_applicant
      val_college hcollegeStrict s, ?_⟩
  rcases hactive with ⟨a, ha⟩
  rcases nextCollege_eq_some_of_active quota val_applicant val_college
      hcollegeStrict s a ha with ⟨c, hcNext, hcUntried, _hcBest⟩
  intro heq
  have hpairOld : (a, c) ∈ untriedEligiblePairs
      val_applicant val_college s :=
    (mem_untriedEligiblePairs_iff val_applicant val_college s a c).2 hcUntried
  have hpairNew : (a, c) ∈ untriedEligiblePairs val_applicant val_college
      (sourceStep quota val_applicant val_college hcollegeStrict s) := by
    rw [heq]
    exact hpairOld
  have hnotApplied := (Finset.mem_filter.mp hpairNew).2.2
  apply hnotApplied
  have hnew : a ∈ newApplications quota val_applicant val_college
      hcollegeStrict s c :=
    (mem_newApplications_iff quota val_applicant val_college
      hcollegeStrict s a c).2 hcNext
  simp [sourceStep, hnew]

theorem untriedEligiblePairs_card_sourceStep_lt_of_active
    (quota : Colleges -> Nat)
    (val_applicant : Applicants -> Colleges -> Real)
    (val_college : Colleges -> Applicants -> Real)
    (hcollegeStrict : forall c a a',
      val_college c a = val_college c a' -> a = a')
    (s : SourceWaitingListState Applicants Colleges)
    (hactive : exists a, SourceActive quota val_applicant val_college
      hcollegeStrict s a) :
    (untriedEligiblePairs val_applicant val_college
      (sourceStep quota val_applicant val_college hcollegeStrict s)).card <
      (untriedEligiblePairs val_applicant val_college s).card :=
  Finset.card_lt_card
    (untriedEligiblePairs_sourceStep_ssubset_of_active quota val_applicant
      val_college hcollegeStrict s hactive)

/-- Run source rounds until no unmatched applicant can make another application. -/
noncomputable def sourceRunToTerminal
    (quota : Colleges -> Nat)
    (val_applicant : Applicants -> Colleges -> Real)
    (val_college : Colleges -> Applicants -> Real)
    (hcollegeStrict : forall c a a',
      val_college c a = val_college c a' -> a = a') :
    SourceWaitingListState Applicants Colleges ->
      SourceWaitingListState Applicants Colleges
  | s => by
      classical
      exact if hactive : exists a, SourceActive quota val_applicant val_college
            hcollegeStrict s a then
          sourceRunToTerminal quota val_applicant val_college hcollegeStrict
            (sourceStep quota val_applicant val_college hcollegeStrict s)
        else s
termination_by s =>
  (untriedEligiblePairs val_applicant val_college s).card
decreasing_by
  apply untriedEligiblePairs_card_sourceStep_lt_of_active
  assumption

theorem sourceRunToTerminal_preserves_invariant
    (quota : Colleges -> Nat)
    (val_applicant : Applicants -> Colleges -> Real)
    (val_college : Colleges -> Applicants -> Real)
    (hcollegeStrict : forall c a a',
      val_college c a = val_college c a' -> a = a')
    (s : SourceWaitingListState Applicants Colleges)
    (hinv : SourceStateInvariant quota val_applicant val_college
      hcollegeStrict s) :
    SourceStateInvariant quota val_applicant val_college hcollegeStrict
      (sourceRunToTerminal quota val_applicant val_college
        hcollegeStrict s) := by
  rw [sourceRunToTerminal]
  split
  next hactive =>
    exact sourceRunToTerminal_preserves_invariant quota val_applicant
      val_college hcollegeStrict
      (sourceStep quota val_applicant val_college hcollegeStrict s)
      (sourceStep_preserves_invariant quota val_applicant val_college
        hcollegeStrict s hinv)
  next hnot =>
    exact hinv
termination_by
  (untriedEligiblePairs val_applicant val_college s).card
decreasing_by
  apply untriedEligiblePairs_card_sourceStep_lt_of_active
  assumption

/-- Terminal direct source state from the empty application history on strict applicant lists. -/
noncomputable def sourceWaitingListFinalState
    (quota : Colleges -> Nat)
    (val_applicant : Applicants -> Colleges -> Real)
    (val_college : Colleges -> Applicants -> Real)
    (hcollegeStrict : forall c a a',
      val_college c a = val_college c a' -> a = a')
    (happlicantStrict : forall a c c',
      val_applicant a c = val_applicant a c' -> c = c') :
    SourceWaitingListState Applicants Colleges :=
  sourceRunToTerminal quota val_applicant val_college hcollegeStrict
    (initialSourceState (Applicants := Applicants) (Colleges := Colleges))

theorem sourceWaitingListFinalState_invariant
    (quota : Colleges -> Nat)
    (val_applicant : Applicants -> Colleges -> Real)
    (val_college : Colleges -> Applicants -> Real)
    (hcollegeStrict : forall c a a',
      val_college c a = val_college c a' -> a = a')
    (happlicantStrict : forall a c c',
      val_applicant a c = val_applicant a c' -> c = c') :
    SourceStateInvariant quota val_applicant val_college hcollegeStrict
      (sourceWaitingListFinalState quota val_applicant val_college
        hcollegeStrict happlicantStrict) :=
  sourceRunToTerminal_preserves_invariant quota val_applicant val_college
    hcollegeStrict _
    (initialSourceState_invariant quota val_applicant val_college hcollegeStrict)

/-- Every rejected application is impossible in every stable assignment. -/
def SourceRejectedPairImpossible
    (quota : Colleges -> Nat)
    (val_applicant : Applicants -> Colleges -> Real)
    (val_college : Colleges -> Applicants -> Real)
    (hcollegeStrict : forall c a a',
      val_college c a = val_college c a' -> a = a')
    (s : SourceWaitingListState Applicants Colleges) : Prop :=
  forall nu : ManyToOneAssignment Applicants Colleges,
    ManyToOne.IsStable val_applicant val_college quota nu ->
    forall a c, a ∈ s.applications c ->
      a ∉ waitingList quota val_college hcollegeStrict s c ->
      nu.app_match a ≠ some c

/-- Convert an invariant direct waiting-list state into a many-to-one assignment. -/
noncomputable def sourceAssignmentFromState
    (quota : Colleges -> Nat)
    (val_applicant : Applicants -> Colleges -> Real)
    (val_college : Colleges -> Applicants -> Real)
    (hcollegeStrict : forall c a a',
      val_college c a = val_college c a' -> a = a')
    (s : SourceWaitingListState Applicants Colleges)
    (hinv : SourceStateInvariant quota val_applicant val_college
      hcollegeStrict s) : ManyToOneAssignment Applicants Colleges where
  app_match := assignedCollege quota val_college hcollegeStrict s
  college_roster := waitingList quota val_college hcollegeStrict s
  consistent a c :=
    assignedCollege_eq_some_iff quota val_applicant val_college
      hcollegeStrict s hinv a c

/-- The assignment returned by the literal Section 4 runner on strict applicant lists. -/
noncomputable def sourceWaitingListFinalAssignment
    (quota : Colleges -> Nat)
    (val_applicant : Applicants -> Colleges -> Real)
    (val_college : Colleges -> Applicants -> Real)
    (hcollegeStrict : forall c a a',
      val_college c a = val_college c a' -> a = a')
    (happlicantStrict : forall a c c',
      val_applicant a c = val_applicant a c' -> c = c') :
    ManyToOneAssignment Applicants Colleges :=
  sourceAssignmentFromState quota val_applicant val_college hcollegeStrict
    (sourceWaitingListFinalState quota val_applicant val_college hcollegeStrict
      happlicantStrict)
    (sourceWaitingListFinalState_invariant quota val_applicant
      val_college hcollegeStrict happlicantStrict)

/-
Applicant-positive but college-negative cloned-seat proposals do not require a
source application.  They are rejected by college individual rationality, so
the common applicant-optimal stable assignment still identifies the outcomes.
-/

end ExactCollegeBatchedProcedure
end GS62CollegeAdmissions
Source
https://github.com/nikhgarg/AppliedModelingLib/blob/e952266be81e96bbeecea6af83d639af324a4438/papers/GS62CollegeAdmissions/ExactCollegeBatchedProcedure.lean#L29-L1222
View graph