The initial proposal budget bounds the number of active steps

Proved

AppliedModelingLib.Matching.no_active_after_steps_of_count_le_length

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, and let $s$ be any consistent deferred-acceptance state. Its remaining proposal budget is $R(s)=\sum_{m\in M}|P_m|$ . Let $L$ be any finite list of natural numbers; only its length matters, since each entry triggers the same state update. If $R(s)\le |L|$ , then

\neg\exists m\in M:\operatorname{Active}\bigl(m,\operatorname{step}^{|L|}(s)\bigr).

Here activity means being unmatched with an acceptable untried woman. This gives a finite termination bound without assuming the stability invariants.

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.no_active_after_steps_of_count_le_length
    (val_m : M → W → ℝ) (val_w : W → M → ℝ)
    (steps : List ℕ) (s : DAState M W)
    (hcount : remainingProposalCount s ≤ steps.length) :
    ¬ ∃ m, IsActiveMan val_m
      (steps.foldl (fun s _ => daStep val_m val_w s) s) m := by sorry

Source

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

View graph