An accepted proposal preserves the deferred-acceptance invariants

Proved

AppliedModelingLib.Matching.acceptStep_preserves_invariants

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)$ and $v_w(m)$ and outside-option value zero. A state $s$ records consistent tentative partners and each man's remaining proposal set. Its invariant $I(s)$ requires individual rationality on both sides, removal of matched pairs from remaining proposals, protection against previously rejected pairs, and proposals in descending preference order.

Suppose $I(s)$ holds, man $m$ is unmatched and has an acceptable remaining proposal, and $w$ is one of his highest-valued remaining acceptable women. Suppose $w$ accepts: she is unmatched and $v_w(m)\ge0$ , or strictly prefers $m$ to her current partner. Form $s'$ by matching $m$ to $w$ , freeing her former partner when one exists, and removing this proposal from $m$ 's remaining set. Then

I(s').

This verifies the acceptance branch of the state update, allowing arbitrary real-valued preferences and ties.

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.acceptStep_preserves_invariants
    (val_m : M → W → ℝ) (val_w : W → M → ℝ)
    (s : DAState M W) {m : M} {w : W}
    (hact : IsActiveMan val_m s m)
    (hwbest : BestRemainingWoman val_m s m w)
    (haccept :
      match s.w_match w with
      | none => 0 ≤ val_w w m
      | some m' => val_w w m' < val_w w m)
    (hinv : DAInvariants val_m val_w s) :
    DAInvariants val_m val_w
      { m_match := fun m'' =>
          if m'' = m then some w
          else if s.w_match w = some m'' then none
          else s.m_match m''
        w_match := Function.update s.w_match w (some m)
        m_proposals := removeProposal s m w
        consistent := by
          simpa using acceptMatch_consistent s hact.1 } := by sorry

Source

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

View graph