A terminated deferred-acceptance state is stable

Proved

AppliedModelingLib.Matching.stable_of_invariants_and_terminated

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

aml-gs62-stable-marriage-20260915game-theorystable-matching

Let $M,W$ be finite sets, with real-valued preferences $u_m(w),v_w(m)$ and outside-option value zero. Let $s$ be a consistent tentative matching with remaining proposal sets, satisfying the five deferred-acceptance invariants: individual rationality on each side, proposal removal for matched pairs, protection against rejected pairs, and descending proposal order. Suppose no unmatched man has a remaining woman whom he values at least zero. The matching $\mu_s$ given by the state's partner maps then satisfies

\mu_s\text{ is individually rational and has no pair }(m,w) \text{ that strictly prefers each other to their assigned outcomes}.

This is the stability conclusion used at the end of the algorithm; strict preferences and equal market sizes are not required for this intermediate lemma.

Preamble

import Mathlib.Algebra.BigOperators.Ring.Finset
import Mathlib.Algebra.Order.BigOperators.Group.Finset
import Mathlib.Data.Finset.Basic
import Mathlib.Data.Finset.Max
import Mathlib.Data.Fintype.Basic
import Mathlib.Data.Fintype.Card
import Mathlib.Data.Fintype.Perm
import Mathlib.Data.Real.Basic
import Mathlib.Tactic.Linarith
import Definitions.Def_AMLGS62_AppliedModelingLib_Markets_Matching_DeferredAcceptance

open AppliedModelingLib
open AppliedModelingLib.Matching

variable {M W : Type*} [Fintype M] [Fintype W] [DecidableEq M] [DecidableEq W]

set_option linter.unusedSimpArgs false

set_option linter.unusedSimpArgs true

-- DA algorithm fold

set_option linter.unusedSimpArgs false

set_option linter.unusedSimpArgs true

Formal statement

theorem AppliedModelingLib.Matching.stable_of_invariants_and_terminated (val_m : M → W → ℝ) (val_w : W → M → ℝ) (s : DAState M W)
    (hinv : DAInvariants val_m val_w s)
    (hterm : ¬ ∃ m, IsActiveMan val_m s m) :
    IsStable val_m val_w ⟨s.m_match, s.w_match, s.consistent⟩ := by sorry

Source

Supporting lemma in the AppliedModelingLib deferred-acceptance formalization; https://github.com/nikhgarg/AppliedModelingLib/blob/e952266be81e96bbeecea6af83d639af324a4438/AppliedModelingLib/Markets/Matching/DeferredAcceptance.lean#L2944-L3000

View graph