Removing an available proposal decreases the proposal budget by one

Proved

AppliedModelingLib.Matching.remainingProposalCount_removeProposal_add_one

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

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

Let $M,W$ be finite sets and let a state $s$ give each man $x\in M$ a finite remaining proposal set $P_x\subseteq W$ . Define

R(s)=\sum_{x\in M}|P_x|.

If $w\in P_m$ , replace $P_m$ by $P_m\setminus\{w\}$ and leave every other proposal set unchanged, obtaining proposal sets $P'_x$ . Then

\sum_{x\in M}|P'_x|+1=R(s).

This is the finite counting identity behind termination of deferred acceptance.

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

Formal statement

theorem AppliedModelingLib.Matching.remainingProposalCount_removeProposal_add_one
    (s : DAState M W) {m : M} {w : W}
    (hw : w ∈ s.m_proposals m) :
    (∑ m' : M, ((removeProposal s m w) m').card) + 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#L1221-L1247

View graph