Every active deferred-acceptance step consumes one proposal

Proved

AppliedModelingLib.Matching.remainingProposalCount_daStep_add_one_of_active

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 and outside-option value zero. Let $s$ be a consistent state with remaining proposal sets $P_m$ , and write $R(s)=\sum_{m\in M}|P_m|$ . A man is active when he is unmatched and has an untried woman whom he values at least zero. If an active man exists, one deferred-acceptance update satisfies

R(\operatorname{step}(s))+1=R(s).

The update chooses an active man and one of his highest-valued acceptable remaining women. The identity holds whether she accepts or rejects him, and supplies an exact termination measure.

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.remainingProposalCount_daStep_add_one_of_active
    (val_m : M → W → ℝ) (val_w : W → M → ℝ) (s : DAState M W)
    (hactive : ∃ m, IsActiveMan val_m s m) :
    remainingProposalCount (daStep val_m val_w s) + 1 =
      remainingProposalCount s := by sorry

Source

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

View graph