Deferred acceptance matches everyone in a balanced, all-acceptable market

Proved

AppliedModelingLib.Matching.deferredAcceptance_complete_of_card_eq_all_pairs_acceptable

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 $|M|=|W|$ . Let $u_m(w),v_w(m)$ be real-valued preferences such that every potential pair is strictly preferable to being unmatched:

u_m(w)>0,\qquad v_w(m)>0\qquad(m\in M,\ w\in W).

The deferred-acceptance outcome $\mu$ is complete on both sides:

\bigl(\forall m\in M,\ \exists w\in W:\mu_M(m)=w\bigr) \ \land\ \bigl(\forall w\in W,\ \exists m\in M:\mu_W(w)=m\bigr).

This completeness lemma permits ties; strict rankings enter only when stating the paper's marriage domain.

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.deferredAcceptance_complete_of_card_eq_all_pairs_acceptable
    (val_m : M → W → ℝ) (val_w : W → M → ℝ)
    (hcard : Fintype.card M = Fintype.card W)
    (hacceptable : AllPairsAcceptable val_m val_w) :
    (∀ m, ∃ w, (deferredAcceptance val_m val_w).m_match m = some w) ∧
      (∀ w, ∃ m, (deferredAcceptance val_m val_w).w_match w = some m) := by sorry

Source

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

View graph