The strict, complete marriage domain

Definition

AMLGS62_GS62CollegeAdmissions_MainTheorems

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

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

Let $M,W$ be sets with real-valued preferences $u_m(w)$ and $v_w(m)$ . The strict marriage domain requires each individual's values for distinct potential partners to be distinct, and every potential pair to be strictly preferable to the outside option:

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

The bundle gives paper-facing names to stability and completeness. Stability means individual rationality and absence of a pair that strictly improves both participants' outcomes; completeness means that both optional partner maps always assign a partner. Finiteness and equality of the two sides' cardinalities are hypotheses of the existence theorem, rather than part of this domain predicate.

Definition code

import Mathlib.Algebra.BigOperators.Ring.Finset
import Mathlib.Algebra.Order.BigOperators.Group.Finset
import Mathlib.Data.Finset.Basic
import Mathlib.Data.Finset.Card
import Mathlib.Data.Finset.Max
import Mathlib.Data.Fintype.Basic
import Mathlib.Data.Fintype.Card
import Mathlib.Data.Fintype.Perm
import Mathlib.Data.Fintype.Sigma
import Mathlib.Data.Real.Basic
import Mathlib.Tactic.Linarith
import Definitions.Def_AMLGS62_AppliedModelingLib_Markets_Matching_Basic
import Definitions.Def_AMLGS62_AppliedModelingLib_Markets_Matching_DeferredAcceptance

namespace GS62CollegeAdmissions
open AppliedModelingLib.Matching

/--
Gale-Shapley strict marriage domain: equal-size one-to-one markets with strict
preferences and every potential pair acceptable.  The paper assumes strict
rankings and no unmatched agents in the marriage story; positivity encodes the
absence of an outside option in the reusable optional-partner API.
-/
def gs_strict_marriage_domain {M W : Type*}
    (val_m : M → W → ℝ) (val_w : W → M → ℝ) : Prop :=
  MenStrictPreferenceProfile val_m ∧
    WomenStrictPreferenceProfile val_w ∧
    AllPairsAcceptable val_m val_w

/-- Paper-facing stable marriage predicate. -/
def gs_stable_marriage {M W : Type*}
    (val_m : M → W → ℝ) (val_w : W → M → ℝ)
    (mu : Assignment M W) : Prop :=
  IsStable val_m val_w mu

/-- Paper-facing complete marriage predicate. -/
def gs_complete_marriage {M W : Type*} (mu : Assignment M W) : Prop :=
  (∀ m, ∃ w, mu.m_match m = some w) ∧
    (∀ w, ∃ m, mu.w_match w = some m)

end GS62CollegeAdmissions

Source

https://github.com/nikhgarg/AppliedModelingLib/blob/e952266be81e96bbeecea6af83d639af324a4438/papers/GS62CollegeAdmissions/MainTheorems.lean#L19-L40

View graph