Stable marriage problem

AbbreviationStrict preference order#✓fully proved

A strict total order on a type \(\alpha\) is a binary relation \(<\) on \(\alpha\) that is irreflexive (\(a < a\) holds for no \(a\)), transitive (\(a < b\) and \(b < c\) imply \(a < c\)) and total on distinct elements (\(a \ne b\) implies \(a < b\) or \(b < a\)). In the Gale–Shapley development it models strict preference.

abbrev StrictTotalOrder := MathlibExt.Order.StrictTotalOrder
Uses 1 · Used by 10
Statement usesStrict total order
Used byGale-Shapley serves every preference profile with \(n\) proposers and \(n\) receivers · Strict total orders are determined by their relation · Existence of stable perfect matchings · Irreflexivity of a strict total order · Relation of a strict total order · Building a strict total order from a relation · Men's preferences · Strict total orders are total on distinct elements · Transitivity of a strict total order · Women's preference profile

AbbreviationBuilding a strict total order from a relation#✓fully proved

A binary relation \(<\) on a set \(\alpha\) that is irreflexive (\(a \not< a\) for all \(a\)), transitive (\(a < b\) and \(b < c\) imply \(a < c\)) and total on distinct elements (\(a \ne b\) implies \(a < b\) or \(b < a\)) defines a strict total order on \(\alpha\) whose relation is \(<\).

abbrev mk {α : Type*} (lt : α → α → Prop)
    (irrefl : ∀ a, ¬lt a a)
    (trans : ∀ {a b c}, lt a b → lt b c → lt a c)
    (total : ∀ {a b}, a ≠ b → lt a b ∨ lt b a) :
    StrictTotalOrder α :=
  MathlibExt.Order.StrictTotalOrder.mk lt irrefl trans total
Uses 2
Statement usesStrict preference order · Strict total order

AbbreviationRelation of a strict total order#✓fully proved

The relation of a strict total order \(T\) on a set \(\alpha\) is its underlying binary relation \(\lt _T\) on \(\alpha\), which is irreflexive, transitive, and relates any two distinct elements in one direction or the other.

abbrev lt {α : Type*} (self : StrictTotalOrder α) : α → α → Prop :=
  MathlibExt.Order.StrictTotalOrder.lt self
Uses 2 · Used by 11
Statement usesStrict preference order · Strict total order
Used byGale-Shapley serves every preference profile with \(n\) proposers and \(n\) receivers · Proposer-optimality · Receiver-pessimality · The Gale-Shapley matching is stable · A stable matching has no blocking pair · Strict total orders are determined by their relation · Existence of stable perfect matchings · Irreflexivity of a strict total order · Blocking pair · Strict total orders are total on distinct elements · Transitivity of a strict total order

AbbreviationIrreflexivity of a strict total order#✓fully proved

Let \(T\) be a strict total order on a set \(\alpha\), with relation \(\lt _T\). Then \(a \lt _T a\) fails for every \(a \in \alpha\).

abbrev irrefl {α : Type*} (self : StrictTotalOrder α) (a : α) : ¬self.lt a a :=
  MathlibExt.Order.StrictTotalOrder.irrefl self a
Uses 3 · Used by 1
Statement usesStrict preference order · Relation of a strict total order · Strict total order
Used byExistence of stable perfect matchings

AbbreviationTransitivity of a strict total order#✓fully proved

Let \(<\) be the relation of a strict total order on a type \(\alpha\). If \(a, b, c \in \alpha\) satisfy \(a < b\) and \(b < c\), then \(a < c\).

abbrev trans {α : Type*} (self : StrictTotalOrder α) {a b c : α}
    (h1 : self.lt a b) (h2 : self.lt b c) : self.lt a c :=
  MathlibExt.Order.StrictTotalOrder.trans self h1 h2
Uses 3 · Used by 1
Statement usesStrict preference order · Relation of a strict total order · Strict total order
Used byExistence of stable perfect matchings

AbbreviationStrict total orders are total on distinct elements#✓fully proved

Let \(<\) be the relation of a strict total order on a type \(\alpha\). If \(a, b \in \alpha\) and \(a \ne b\), then \(a < b\) or \(b < a\).

abbrev total {α : Type*} (self : StrictTotalOrder α) {a b : α} (h : a ≠ b) :
    self.lt a b ∨ self.lt b a :=
  MathlibExt.Order.StrictTotalOrder.total self h
Uses 3 · Used by 1
Statement usesStrict preference order · Relation of a strict total order · Strict total order
Used byExistence of stable perfect matchings

TheoremStrict total orders are determined by their relation#✓fully proved

Let \(T\) and \(T'\) be strict total orders on a set \(\alpha\), with relations \(\lt _T\) and \(\lt _{T'}\). If \(x \lt _T y \iff x \lt _{T'} y\) for all \(x, y \in \alpha\), then \(T = T'\).

@[ext]
theorem ext {α : Type*} {T T' : StrictTotalOrder α} (h : T.lt = T'.lt) :
    T = T'
Uses 3
Statement usesStrict preference order · Relation of a strict total order
Proof usesStrict total orders are determined by their relation

AbbreviationMen's preferences#✓fully proved

For sets \(M\) (men) and \(W\) (women), a preference profile of the men assigns to each \(m \in M\) a strict total order on \(W\), the preferences of \(m\).

abbrev MPrefs (M W : Type*) := M → StrictTotalOrder W
Uses 1 · Used by 7
Statement usesStrict preference order
Used byGale-Shapley serves every preference profile with \(n\) proposers and \(n\) receivers · Proposers' preferences from rankings · Gale–Shapley theorem · Existence of stable perfect matchings · Blocking pair · Stable perfect matching · Men's preferences induced by rankings

AbbreviationWomen's preference profile#✓fully proved

For types \(M\) and \(W\), a preference profile of \(W\) over \(M\) assigns to each \(w \in W\) a strict total order on \(M\), read as the strict preference of \(w\) among the elements of \(M\).

abbrev WPrefs (M W : Type*) := W → StrictTotalOrder M
Uses 1 · Used by 7
Statement usesStrict preference order
Used byGale-Shapley serves every preference profile with \(n\) proposers and \(n\) receivers · Receivers' preference profile from rankings · Gale–Shapley theorem · Existence of stable perfect matchings · Blocking pair · Stable perfect matching · Women's preference orders of a profile

AbbreviationPerfect matching#✓fully proved

A perfect matching between sets \(M\) and \(W\) is a bijection \(\mu \colon M \to W\), which matches each \(m \in M\) with \(\mu(m) \in W\).

abbrev PerfectMatching (M W : Type*) := M ≃ W
Used by 14
Used byA proposer's final partner is his last proposal · Gale-Shapley serves every preference profile with \(n\) proposers and \(n\) receivers · The Gale-Shapley matching · Proposer-optimality · Receiver-pessimality · Invariant of deferred acceptance · The Gale-Shapley matching is stable · Rejected proposals bound stable partners · A stable matching has no blocking pair · Deferred acceptance makes at most n² proposals · Gale–Shapley theorem · Existence of stable perfect matchings · Blocking pair · Stable perfect matching

DefinitionBlocking pair#✓fully proved

Let \(M\) and \(W\) be sets. Suppose that each \(m \in M\) has a strict total order \(\lt _m\) of preference on \(W\) and each \(w \in W\) has a strict total order \(\lt _w\) of preference on \(M\), where \(x \lt _m y\) means that \(m\) prefers \(x\) to \(y\), and likewise for \(\lt _w\). For a perfect matching \(\mu\) between \(M\) and \(W\), a pair \((m, w) \in M \times W\) is a blocking pair when \(w \lt _m \mu(m)\) and \(m \lt _w \mu^{-1}(w)\), that is, when \(m\) prefers \(w\) to \(\mu(m)\) and \(w\) prefers \(m\) to \(\mu^{-1}(w)\).

def IsBlockingPair {M W : Type*}
    (mp : MPrefs M W) (wp : WPrefs M W) (μ : PerfectMatching M W) (m : M) (w : W) : Prop :=
  (mp m).lt w (μ m) ∧ (wp w).lt m (μ.symm w)
Uses 4 · Used by 3
Statement usesMen's preferences · Perfect matching · Relation of a strict total order · Women's preference profile
Used byThe Gale-Shapley matching is stable · Existence of stable perfect matchings · Stable perfect matching

DefinitionStable perfect matching#✓fully proved

Let \(M\) and \(W\) be sets. Suppose that each \(m \in M\) has a strict total order of preference on \(W\) and each \(w \in W\) has a strict total order of preference on \(M\). A perfect matching \(\mu\) between \(M\) and \(W\) is stable for these preferences when no pair \((m, w) \in M \times W\) is a blocking pair for \(\mu\).

def IsStable {M W : Type*} (mp : MPrefs M W) (wp : WPrefs M W) (μ : PerfectMatching M W) : Prop :=
  ∀ m w, ¬ IsBlockingPair mp wp μ m w
Uses 4 · Used by 13
Statement usesBlocking pair · Men's preferences · Perfect matching · Women's preference profile
Used byA proposer's final partner is his last proposal · Gale-Shapley serves every preference profile with \(n\) proposers and \(n\) receivers · The Gale-Shapley matching · Proposer-optimality · Receiver-pessimality · Invariant of deferred acceptance · The Gale-Shapley matching is stable · Rejected proposals bound stable partners · A stable matching has no blocking pair · Deferred acceptance makes at most n² proposals · Gale–Shapley theorem · Existence of stable perfect matchings · Stable matching

TheoremExistence of stable perfect matchings#✓fully proved

Let \(M\) and \(W\) be finite sets with the same number of elements. Suppose that each \(m \in M\) has a strict total order of preference on \(W\) and each \(w \in W\) has a strict total order of preference on \(M\). Then some perfect matching between \(M\) and \(W\) is stable for these preferences.

This is the Gale–Shapley theorem, stated without decidability assumptions on \(M\) and \(W\).

theorem gale_shapley_exists_stable_matching_general
    {M W : Type*} [Fintype M] [Fintype W]
    (hCard : Fintype.card M = Fintype.card W)
    (mp : MPrefs M W) (wp : WPrefs M W) :
    ∃ μ : PerfectMatching M W, IsStable mp wp μ
Uses 10 · Used by 1
Statement usesStable perfect matching · Men's preferences · Perfect matching · Women's preference profile
Proof usesBlocking pair · Strict preference order · Irreflexivity of a strict total order · Relation of a strict total order · Strict total orders are total on distinct elements · Transitivity of a strict total order
Used byGale–Shapley theorem

TheoremGale–Shapley theorem#✓fully proved

Let \(M\) and \(W\) be finite sets with the same number of elements. Suppose that each \(m \in M\) has a strict total order of preference on \(W\) and each \(w \in W\) has a strict total order of preference on \(M\). Then some perfect matching between \(M\) and \(W\) is stable for these preferences.

@[nolint unusedArguments]
theorem gale_shapley_exists_stable_matching
    {M W : Type*} [Fintype M] [Fintype W] [DecidableEq M] [DecidableEq W]
    (hCard : Fintype.card M = Fintype.card W)
    (mp : MPrefs M W) (wp : WPrefs M W) :
    ∃ μ : PerfectMatching M W, IsStable mp wp μ
Sources
  • D. Gale and L. S. Shapley, "College Admissions and the Stability of Marriage", American Mathematical Monthly 69 (1962), 9–15, DOI 10.2307/2312726. It follows from gale_shapley_exists_stable_matching_general; the instances [DecidableEq M] and [DecidableEq W] are unused and keep the source's shape.
Uses 5
Statement usesStable perfect matching · Men's preferences · Perfect matching · Women's preference profile
Proof usesExistence of stable perfect matchings

AbbreviationPreference profile for \(n\) men and \(n\) women#✓fully proved

For a natural number \(n\), number \(n\) men and \(n\) women by \(0, \dots, n - 1\). A preference profile \(P = (M, W)\) for them consists of a permutation \(M_i\) of \(\{0, \dots, n - 1\}\) for each man \(i\) and a permutation \(W_j\) of \(\{0, \dots, n - 1\}\) for each woman \(j\): \(M_i(r)\) is the woman man \(i\) ranks at zero-based position \(r\), and \(W_j(r)\) is the man woman \(j\) ranks at position \(r\).

abbrev PreferenceProfile (n : ℕ) : Type :=
  (Fin n → Equiv.Perm (Fin n)) × (Fin n → Equiv.Perm (Fin n))
Sources
  • Borodin, Duncan, Litchev, Liu, Moroz, Qian, Raghavan, Rastogi, Voigt, and Khovanova, Sequences of the Stable Matching Problem, Journal of Integer Sequences 27 (2024), Article 24.2.2, Section 2.
Used by 26
Used byCounting disjoint preference profiles · Number of Gale–Shapley rounds · When the Gale–Shapley algorithm ends in one round · Gale–Shapley rounds when all men have the same preferences · Gale–Shapley rounds with no participants · Proposal counts in the Gale–Shapley algorithm · One round of the Gale–Shapley algorithm · No proposals before the first round · Provisional engagement in the Gale–Shapley algorithm · A hell-couple belongs to every stable matching · At most one hell-couple in a stable matching · Hell-couple · Soulmate pair · Stable matching · Stability in terms of ranks · Men's preferences induced by rankings · Rank of a woman for a man · Profiles with Latin-square men's preferences, counted by soulmate pairs · Mutually Latin profiles with \(k\) soulmate pairs · Profiles with a pair of outcasts · Number of soulmate pairs · A profile has at most \(n\) soulmate pairs · Number of profiles with exactly \(k\) soulmate pairs · Profiles with \(n - 1\) soulmate pairs · Women's preference orders of a profile · A woman's rank of a man

DefinitionRank of a woman for a man#✓fully proved

For a preference profile of \(n\) men and \(n\) women, the rank of woman \(j\) for man \(i\) is the zero-based position \(r \in \{0, \dots, n-1\}\) at which \(i\) ranks \(j\), so his favorite has rank \(0\) and his least favorite has rank \(n - 1\).

The paper's one-based ranking is this rank plus one.

def manRank (P : PreferenceProfile n) (i j : Fin n) : ℕ :=
  ((P.1 i).symm j : ℕ)
Sources
  • Borodin et al., Sequences of the Stable Matching Problem, Journal of Integer Sequences 27 (2024), Article 24.2.2, Section 2.
Uses 1 · Used by 7
Statement usesPreference profile for \(n\) men and \(n\) women
Used byHell-couple · Soulmate pair · Stability in terms of ranks · Men's preferences induced by rankings · Profiles with a pair of outcasts · A profile has at most \(n\) soulmate pairs · Profiles with \(n - 1\) soulmate pairs

DefinitionA woman's rank of a man#✓fully proved

For a preference profile for \(n\) men and \(n\) women, the rank that woman \(j\) gives man \(i\) is the zero-based position at which she ranks him, that is, the paper's ranking minus one.

def womanRank (P : PreferenceProfile n) (j i : Fin n) : ℕ :=
  ((P.2 j).symm i : ℕ)
Sources
  • Borodin et al., Sequences of the Stable Matching Problem, Journal of Integer Sequences 27 (2024), Article 24.2.2, Section 2.
Uses 1 · Used by 7
Statement usesPreference profile for \(n\) men and \(n\) women
Used byProvisional engagement in the Gale–Shapley algorithm · Hell-couple · Soulmate pair · Stability in terms of ranks · Profiles with a pair of outcasts · A profile has at most \(n\) soulmate pairs · Women's preference orders of a profile

DefinitionSoulmate pair#✓fully proved

For a preference profile of \(n\) men and \(n\) women, man \(i\) and woman \(j\) are soulmates when each ranks the other first: \(j\) is the first choice of \(i\) and \(i\) is the first choice of \(j\).

def IsSoulmatePair (P : PreferenceProfile n) (i j : Fin n) : Prop :=
  manRank P i j = 0 ∧ womanRank P j i = 0
Sources
  • Borodin et al., Sequences of the Stable Matching Problem, Journal of Integer Sequences 27 (2024), Article 24.2.2, Section 2.1.
Uses 3 · Used by 3
Statement usesPreference profile for \(n\) men and \(n\) women · Rank of a woman for a man · A woman's rank of a man
Used byNumber of soulmate pairs · A profile has at most \(n\) soulmate pairs · Profiles with \(n - 1\) soulmate pairs

DefinitionNumber of soulmate pairs#✓fully proved

The number of soulmate pairs of a preference profile \(P\) for \(n\) men and \(n\) women is the number of pairs \((i, j)\) of a man \(i\) and a woman \(j\) that are soulmates in \(P\), that is, each ranks the other first.

This is the paper's \(k\) in \(F(k, n)\), the number of profiles with exactly \(k\) soulmate pairs.

noncomputable def soulmatePairCount (P : PreferenceProfile n) : ℕ :=
  Nat.card {ij : Fin n × Fin n // IsSoulmatePair P ij.1 ij.2}
Sources
  • Borodin et al., Sequences of the Stable Matching Problem, Journal of Integer Sequences 27 (2024), Article 24.2.2, Section 4.
Uses 2 · Used by 5
Statement usesSoulmate pair · Preference profile for \(n\) men and \(n\) women
Used byProfiles with Latin-square men's preferences, counted by soulmate pairs · Mutually Latin profiles with \(k\) soulmate pairs · A profile has at most \(n\) soulmate pairs · Number of profiles with exactly \(k\) soulmate pairs · Profiles with \(n - 1\) soulmate pairs

DefinitionMen's preferences induced by rankings#✓fully proved

For a preference profile of \(n\) men and \(n\) women, each man \(i\) gets the strict total order on the women in which \(i\) prefers woman \(a\) to woman \(b\) exactly when he ranks \(a\) at an earlier position than \(b\).

def manPrefs (P : PreferenceProfile n) :
    MathlibExt.Combinatorics.Matching.GaleShapley.MPrefs (Fin n) (Fin n) := fun i =>
  { lt := fun a b => manRank P i a < manRank P i b
    irrefl := fun a => lt_irrefl _
    trans := fun h1 h2 => lt_trans h1 h2
    total := fun {a b} hab => by
      rcases lt_trichotomy (manRank P i a) (manRank P i b) with h | h | h
      · exact Or.inl h
      · exact absurd ((P.1 i).symm.injective (Fin.ext h)) hab
      · exact Or.inr h }
Sources
  • Borodin et al., Sequences of the Stable Matching Problem, Journal of Integer Sequences 27 (2024), Article 24.2.2, Section 2.
Uses 4 · Used by 1
Statement usesMen's preferences · Strict total order · Preference profile for \(n\) men and \(n\) women · Rank of a woman for a man
Used byStable matching

DefinitionWomen's preference orders of a profile#✓fully proved

For a preference profile \(P\) for \(n\) men and \(n\) women, each woman \(j\) gets the strict total order on the men in which man \(a\) comes before (is preferred to) man \(b\) exactly when woman \(j\) ranks \(a\) at an earlier position than \(b\).

def womanPrefs (P : PreferenceProfile n) :
    MathlibExt.Combinatorics.Matching.GaleShapley.WPrefs (Fin n) (Fin n) := fun j =>
  { lt := fun a b => womanRank P j a < womanRank P j b
    irrefl := fun a => lt_irrefl _
    trans := fun h1 h2 => lt_trans h1 h2
    total := fun {a b} hab => by
      rcases lt_trichotomy (womanRank P j a) (womanRank P j b) with h | h | h
      · exact Or.inl h
      · exact absurd ((P.2 j).symm.injective (Fin.ext h)) hab
      · exact Or.inr h }
Sources
  • Borodin et al., Sequences of the Stable Matching Problem, Journal of Integer Sequences 27 (2024), Article 24.2.2, Section 2.
Uses 4 · Used by 1
Statement usesWomen's preference profile · Strict total order · Preference profile for \(n\) men and \(n\) women · A woman's rank of a man
Used byStable matching

AbbreviationStable matching#✓fully proved

For a preference profile of \(n\) men and \(n\) women, a matching \(\mu\), in which man \(i\) marries woman \(\mu(i)\), is stable when no man and woman both strictly prefer each other to their own spouses. Equivalently, \(\mu\) is a stable perfect matching for the strict preferences induced by the men's and the women's rankings.

abbrev IsStableMatching (P : PreferenceProfile n) (μ : Equiv.Perm (Fin n)) : Prop :=
  MathlibExt.Combinatorics.Matching.GaleShapley.IsStable (manPrefs P) (womanPrefs P) μ
Sources
  • Borodin et al., Sequences of the Stable Matching Problem, Journal of Integer Sequences 27 (2024), Article 24.2.2, Section 2.
Uses 4 · Used by 4
Statement usesStable perfect matching · Preference profile for \(n\) men and \(n\) women · Men's preferences induced by rankings · Women's preference orders of a profile
Used byA hell-couple belongs to every stable matching · At most one hell-couple in a stable matching · Stability in terms of ranks · Profiles with \(n - 1\) soulmate pairs

TheoremStability in terms of ranks#✓fully proved

For a preference profile of \(n\) men and \(n\) women, a matching \(\mu\), in which man \(i\) marries woman \(\mu(i)\), is stable if and only if there are no man \(i\) and woman \(j\) such that \(i\) ranks \(j\) strictly above his wife \(\mu(i)\) and \(j\) ranks \(i\) strictly above her husband \(\mu^{-1}(j)\).

theorem isStableMatching_iff (P : PreferenceProfile n) (μ : Equiv.Perm (Fin n)) :
    IsStableMatching P μ ↔ ∀ i j : Fin n,
      ¬ (manRank P i j < manRank P i (μ i) ∧ womanRank P j i < womanRank P j (μ.symm j))
Sources
  • Borodin et al., Sequences of the Stable Matching Problem, Journal of Integer Sequences 27 (2024), Article 24.2.2, Section 2.
Uses 4
Statement usesStable matching · Preference profile for \(n\) men and \(n\) women · Rank of a woman for a man · A woman's rank of a man

DefinitionHell-couple#✓fully proved

Let \(P\) be a preference profile of \(n\) men and \(n\) women, and let \(\mu\) be a matching in which man \(i\) marries woman \(\mu(i)\). Man \(i\) and his wife \(\mu(i)\) form a hell-couple when each ranks the other last: \(i\) ranks \(\mu(i)\) in his last position and \(\mu(i)\) ranks \(i\) in her last position.

def IsHellCouple (P : PreferenceProfile n) (μ : Equiv.Perm (Fin n)) (i : Fin n) : Prop :=
  manRank P i (μ i) = n - 1 ∧ womanRank P (μ i) i = n - 1
Sources
  • Borodin et al., Sequences of the Stable Matching Problem, Journal of Integer Sequences 27 (2024), Article 24.2.2, Section 6.1.
Uses 3 · Used by 2
Statement usesPreference profile for \(n\) men and \(n\) women · Rank of a woman for a man · A woman's rank of a man
Used byA hell-couple belongs to every stable matching · At most one hell-couple in a stable matching

DefinitionNumber of Latin squares#✓fully proved

For \(n \in \mathbb{N}\), \(L_n\) is the number of Latin squares of order \(n\): families \((M_0, \dots, M_{n-1})\) of permutations of \(\{0, \dots, n-1\}\) (the rows) such that for every position \(r\) the entries \(M_0(r), \dots, M_{n-1}(r)\) (column \(r\)) are pairwise distinct.

noncomputable def latinSquareCount (n : ℕ) : ℕ :=
  Nat.card {M : Fin n → Equiv.Perm (Fin n) // ∀ r : Fin n, Function.Injective fun i => M i r}
Sources
  • Borodin et al., Sequences of the Stable Matching Problem, Journal of Integer Sequences 27 (2024), Article 24.2.2, Section 4.2 (OEIS A002860).
Used by 3
Used byLatin squares of order zero · Profiles with Latin-square men's preferences, counted by soulmate pairs · Mutually Latin profiles with \(k\) soulmate pairs

DefinitionProvisional engagement in the Gale–Shapley algorithm#✓fully proved

Let \(P\) be a preference profile for \(n\) men and \(n\) women, with positions in each ranking numbered \(0, \dots, n - 1\), and consider the state of the men-proposing Gale–Shapley algorithm in which each man \(i'\) has proposed to the women at the positions \(r' < p(i')\) of his ranking. Man \(i\) is provisionally engaged in this state if \(1 \le p(i) \le n\) and the woman \(w\) at his position \(p(i) - 1\) (the last woman he proposed to) ranks him weakly above every man who has proposed to her: her position for \(i\) is at most her position for every man \(i'\) who has \(w\) at some position \(r' < p(i')\).

def GSEngaged (P : PreferenceProfile n) (p : Fin n → ℕ) (i : Fin n) : Prop :=
  ∃ r : Fin n, r.val + 1 = p i ∧
    ∀ i' r' : Fin n, r'.val < p i' → P.1 i' r' = P.1 i r →
      womanRank P (P.1 i r) i ≤ womanRank P (P.1 i r) i'
Sources
  • Borodin et al., Sequences of the Stable Matching Problem, Journal of Integer Sequences 27 (2024), Article 24.2.2, Section 2 (description of the Gale–Shapley algorithm).
Uses 2 · Used by 4
Statement usesPreference profile for \(n\) men and \(n\) women · A woman's rank of a man
Used byNumber of Gale–Shapley rounds · Gale–Shapley rounds with no participants · Proposal counts in the Gale–Shapley algorithm · One round of the Gale–Shapley algorithm

DefinitionProposal counts in the Gale–Shapley algorithm#✓fully proved

Let \(P\) be a preference profile for \(n\) men and \(n\) women. The number \(p_t(i)\) of women man \(i\) has proposed to after \(t\) rounds of the men-proposing Gale–Shapley algorithm on \(P\) is defined by \(p_0(i) = 0\) and, for every \(t\), \(p_{t+1}(i) = p_t(i)\) if man \(i\) is provisionally engaged in the state \(p_t\) and \(p_{t+1}(i) = p_t(i) + 1\) otherwise: in each round every man who is not provisionally engaged proposes to his next choice.

noncomputable def gsProposals (P : PreferenceProfile n) : ℕ → Fin n → ℕ
  | 0 => fun _ => 0
  | t + 1 => fun i =>
      if GSEngaged P (gsProposals P t) i then gsProposals P t i else gsProposals P t i + 1
Sources
  • Borodin et al., Sequences of the Stable Matching Problem, Journal of Integer Sequences 27 (2024), Article 24.2.2, Section 2.
Uses 2 · Used by 4
Statement usesProvisional engagement in the Gale–Shapley algorithm · Preference profile for \(n\) men and \(n\) women
Used byNumber of Gale–Shapley rounds · Gale–Shapley rounds with no participants · One round of the Gale–Shapley algorithm · No proposals before the first round

DefinitionNumber of Gale–Shapley rounds#✓fully proved

For a preference profile \(P\) for \(n\) men and \(n\) women, the number of rounds of the men-proposing Gale–Shapley algorithm on \(P\) is the least \(t\) such that every man is provisionally engaged after \(t\) rounds (or \(0\) if there is no such \(t\)).

noncomputable def galeShapleyRounds (P : PreferenceProfile n) : ℕ :=
  sInf {t : ℕ | ∀ i : Fin n, GSEngaged P (gsProposals P t) i}
Sources
  • Borodin et al., Sequences of the Stable Matching Problem, Journal of Integer Sequences 27 (2024), Article 24.2.2, Section 2.
Uses 3 · Used by 4
Statement usesProvisional engagement in the Gale–Shapley algorithm · Preference profile for \(n\) men and \(n\) women · Proposal counts in the Gale–Shapley algorithm
Used byWhen the Gale–Shapley algorithm ends in one round · Gale–Shapley rounds when all men have the same preferences · Gale–Shapley rounds with no participants · Profiles with \(n - 1\) soulmate pairs

TheoremNo proposals before the first round#✓fully proved

For every preference profile, after zero rounds of the men-proposing Gale–Shapley algorithm every man has made zero proposals.

theorem gsProposals_zero (P : PreferenceProfile n) : gsProposals P 0 = fun _ => 0
Sources
  • Borodin et al., Sequences of the Stable Matching Problem, Journal of Integer Sequences 27 (2024), Article 24.2.2, Section 2.
Uses 2
Statement usesPreference profile for \(n\) men and \(n\) women · Proposal counts in the Gale–Shapley algorithm

TheoremOne round of the Gale–Shapley algorithm#✓fully proved

Let \(P\) be a preference profile for \(n\) men and \(n\) women and let \(t\) be a natural number. After \(t + 1\) rounds of the men-proposing Gale–Shapley algorithm on \(P\), a man who is provisionally engaged after \(t\) rounds has made as many proposals as after \(t\) rounds, and every other man has made one proposal more than after \(t\) rounds.

theorem gsProposals_succ (P : PreferenceProfile n) (t : ℕ) (i : Fin n) :
    gsProposals P (t + 1) i =
      if GSEngaged P (gsProposals P t) i then gsProposals P t i
      else gsProposals P t i + 1
Sources
  • Borodin et al., Sequences of the Stable Matching Problem, Journal of Integer Sequences 27 (2024), Article 24.2.2, Section 2.
Uses 3
Statement usesProvisional engagement in the Gale–Shapley algorithm · Preference profile for \(n\) men and \(n\) women · Proposal counts in the Gale–Shapley algorithm

TheoremGale–Shapley rounds with no participants#✓fully proved

For the preference profile with no men and no women, the men-proposing Gale–Shapley algorithm takes zero rounds.

theorem galeShapleyRounds_of_zero (P : PreferenceProfile 0) : galeShapleyRounds P = 0
Sources
  • Borodin et al., Sequences of the Stable Matching Problem, Journal of Integer Sequences 27 (2024), Article 24.2.2, Section 2.
Uses 4
Statement usesPreference profile for \(n\) men and \(n\) women · Number of Gale–Shapley rounds
Proof usesProvisional engagement in the Gale–Shapley algorithm · Proposal counts in the Gale–Shapley algorithm

TheoremA profile has at most \(n\) soulmate pairs#✓fully proved

Every preference profile for \(n\) men and \(n\) women has at most \(n\) soulmate pairs, since a man's soulmate is his first choice.

theorem soulmatePairCount_le (P : PreferenceProfile n) : soulmatePairCount P ≤ n
Sources
  • Borodin et al., Sequences of the Stable Matching Problem, Journal of Integer Sequences 27 (2024), Article 24.2.2, Section 4.
Uses 5
Statement usesPreference profile for \(n\) men and \(n\) women · Number of soulmate pairs
Proof usesSoulmate pair · Rank of a woman for a man · A woman's rank of a man

TheoremLatin squares of order zero#✓fully proved

There is exactly one Latin square of order \(0\), that is, \(L_0 = 1\).

theorem latinSquareCount_zero : latinSquareCount 0 = 1
Sources
  • Borodin et al., Sequences of the Stable Matching Problem, Journal of Integer Sequences 27 (2024), Article 24.2.2, Section 4.2 (OEIS A002860).
Uses 1
Statement usesNumber of Latin squares

TheoremGale–Shapley rounds when all men have the same preferences#●ready to prove

Let \(P\) be a preference profile for \(n\) men and \(n\) women in which all men rank the women in the same order. Then the men-proposing Gale–Shapley algorithm on \(P\) ends in exactly \(n\) rounds.

public theorem_wanted galeShapleyRounds_of_same_taste (P : PreferenceProfile n)
    (h : ∀ i i' : Fin n, P.1 i = P.1 i') :
    galeShapleyRounds P = n
Sources
  • Borodin, Duncan, Litchev, Liu, Moroz, Qian, Raghavan, Rastogi, Voigt, and Khovanova, Sequences of the Stable Matching Problem, Journal of Integer Sequences 27 (2024), Article 24.2.2, Proposition 1 (jis-2024-24.2.2-prop-1).
Uses 2
Statement usesPreference profile for \(n\) men and \(n\) women · Number of Gale–Shapley rounds

TheoremWhen the Gale–Shapley algorithm ends in one round#●ready to prove

Let \(n \ge 1\) and let \(P\) be a preference profile for \(n\) men and \(n\) women. The men-proposing Gale–Shapley algorithm on \(P\) ends in exactly one round if and only if every woman is the first choice of exactly one man.

public theorem_wanted galeShapleyRounds_eq_one_iff (P : PreferenceProfile n) (hn : 0 < n) :
    galeShapleyRounds P = 1 ↔ ∀ j : Fin n, ∃! i : Fin n, P.1 i ⟨0, hn⟩ = j
Sources
  • Borodin et al., Sequences of the Stable Matching Problem, Journal of Integer Sequences 27 (2024), Article 24.2.2, Proposition 2 (jis-2024-24.2.2-prop-2).
Uses 2
Statement usesPreference profile for \(n\) men and \(n\) women · Number of Gale–Shapley rounds

TheoremCounting disjoint preference profiles#●ready to prove

Call a preference profile for \(n\) men and \(n\) women disjoint if for every pair of positions \((r, s)\) there is exactly one man–woman pair in which the man ranks the woman at position \(r\) and the woman ranks the man at position \(s\). For every natural number \(n\), the number of disjoint profiles is at most \((n^2)!\) and is divisible by \((n!)^2\).

public theorem_wanted disjoint_profiles_card_le_and_dvd (n : ℕ) :
    Nat.card {P : PreferenceProfile n //
        Function.Bijective fun ij : Fin n × Fin n => ((P.1 ij.1).symm ij.2, (P.2 ij.2).symm ij.1)} ≤
        (n ^ 2)! ∧
      (n ! ) ^ 2 ∣ Nat.card {P : PreferenceProfile n //
        Function.Bijective fun ij : Fin n × Fin n => ((P.1 ij.1).symm ij.2, (P.2 ij.2).symm ij.1)}
Sources
  • Borodin et al., Sequences of the Stable Matching Problem, Journal of Integer Sequences 27 (2024), Article 24.2.2, Proposition 3 (jis-2024-24.2.2-prop-3).
Uses 1
Statement usesPreference profile for \(n\) men and \(n\) women

TheoremOutsiders without soulmate pairs#●ready to prove

Let \(n\) and \(k\) be natural numbers, where \(n - k\) is read as \(0\) when \(k > n\). Consider the \(n - k\) men \(k, \dots, n - 1\) and the \(n - k\) women \(k, \dots, n - 1\) among \(n\) men and \(n\) women numbered from \(0\), where each of these men ranks all \(n\) women and each of these women ranks all \(n\) men. The number of ways to choose these rankings so that no man and woman among them each rank the other first is

\[\sum_{i=0}^{n-k} (-1)^i \binom{n-k}{i}^2 ((n-1)!)^{2i}\, i!\, (n!)^{2(n-k-i)}.\]

This number is the paper's \(S(k, n)\): the preferences of the remaining \(k\) men and \(k\) women are ignored.

public theorem_wanted outside_no_soulmates_card (n k : ℕ) :
    (Nat.card {MW : (Fin (n - k) → Equiv.Perm (Fin n)) × (Fin (n - k) → Equiv.Perm (Fin n)) //
        ∀ a b : Fin (n - k),
          ¬ (((MW.1 a).symm ⟨k + b.val, by have := b.isLt; omega⟩ : ℕ) = 0 ∧
            ((MW.2 b).symm ⟨k + a.val, by have := a.isLt; omega⟩ : ℕ) = 0)} : ℤ) =
      ∑ i ∈ range (n - k + 1),
        (-1 : ℤ) ^ i * ((n - k).choose i : ℤ) ^ 2 * ((n - 1)! : ℤ) ^ (2 * i) * (i ! : ℤ) *
          (n ! : ℤ) ^ (2 * n - 2 * k - 2 * i)
Sources
  • Borodin et al., Sequences of the Stable Matching Problem, Journal of Integer Sequences 27 (2024), Article 24.2.2, Lemma 4 (jis-2024-24.2.2-lem-4).

TheoremNumber of profiles with exactly \(k\) soulmate pairs#●ready to prove

For natural numbers \(n\) and \(k\), the number \(F(k, n)\) of preference profiles for \(n\) men and \(n\) women with exactly \(k\) soulmate pairs is

\[ \binom{n}{k}^2 k!\, ((n-1)!)^{2k} \sum_{i=0}^{n-k} (-1)^i \binom{n-k}{i}^2 ((n-1)!)^{2i}\, i!\, (n!)^{2(n-k-i)}. \]

When \(k > n\) both sides are \(0\).

The sum is the paper's \(S(k, n)\) of Lemma 4, which counts the preferences of the people outside the \(k\) soulmate couples that create no further soulmate pair.

public theorem_wanted soulmate_profiles_card (n k : ℕ) :
    (Nat.card {P : PreferenceProfile n // soulmatePairCount P = k} : ℤ) =
      (n.choose k : ℤ) ^ 2 * (k ! : ℤ) * ((n - 1)! : ℤ) ^ (2 * k) *
        ∑ i ∈ range (n - k + 1),
          (-1 : ℤ) ^ i * ((n - k).choose i : ℤ) ^ 2 * ((n - 1)! : ℤ) ^ (2 * i) * (i ! : ℤ) *
            (n ! : ℤ) ^ (2 * n - 2 * k - 2 * i)
Sources
  • Borodin et al., Sequences of the Stable Matching Problem, Journal of Integer Sequences 27 (2024), Article 24.2.2, Theorem 6 (jis-2024-24.2.2-thm-6).
Uses 2
Statement usesPreference profile for \(n\) men and \(n\) women · Number of soulmate pairs

TheoremProfiles with \(n - 1\) soulmate pairs#●ready to prove

Let \(P\) be a preference profile for \(n\) men and \(n\) women with exactly \(n - 1\) soulmate pairs (read as \(0\) when \(n = 0\)). Then \(P\) has exactly one stable matching. Moreover, for every stable matching \(\mu\) of \(P\) and every man \(i\) who has no soulmate, the men-proposing Gale–Shapley algorithm on \(P\) ends after \(r + 1\) rounds, where \(r\) is the zero-based position at which man \(i\) ranks his wife \(\mu(i)\).

public theorem_wanted unique_stable_matching_of_soulmatePairCount_eq_pred
    (P : PreferenceProfile n) (h : soulmatePairCount P = n - 1) :
    (∃! μ : Equiv.Perm (Fin n), IsStableMatching P μ) ∧
      ∀ μ : Equiv.Perm (Fin n), IsStableMatching P μ →
        ∀ i : Fin n, (∀ j : Fin n, ¬ IsSoulmatePair P i j) →
          galeShapleyRounds P = manRank P i (μ i) + 1
Sources
  • Borodin et al., Sequences of the Stable Matching Problem, Journal of Integer Sequences 27 (2024), Article 24.2.2, Proposition 7 (jis-2024-24.2.2-prop-7).
Uses 6
Statement usesSoulmate pair · Stable matching · Preference profile for \(n\) men and \(n\) women · Number of Gale–Shapley rounds · Rank of a woman for a man · Number of soulmate pairs

TheoremProfiles with Latin-square men's preferences, counted by soulmate pairs#●ready to prove

For all \(n, k \in \mathbb{N}\), the number of preference profiles of \(n\) men and \(n\) women in which, for every position \(r\), different men rank different women at position \(r\) (the men's rankings form a Latin square), and which have exactly \(k\) soulmate pairs, is

\[L_n \binom{n}{k} (n-1)^{n-k} ((n-1)!)^n,\]

where \(L_n\) is the number of Latin squares of order \(n\).

Here \(n - 1\) and \(n - k\) are truncated subtractions in \(\mathbb{N}\).

public theorem_wanted men_latin_soulmate_profiles_card (n k : ℕ) :
    Nat.card {P : PreferenceProfile n //
        (∀ r : Fin n, Function.Injective fun i => P.1 i r) ∧ soulmatePairCount P = k} =
      latinSquareCount n * n.choose k * (n - 1) ^ (n - k) * ((n - 1)!) ^ n
Sources
  • Borodin et al., Sequences of the Stable Matching Problem, Journal of Integer Sequences 27 (2024), Article 24.2.2, Theorem 8 (jis-2024-24.2.2-thm-8).
Uses 3
Statement usesPreference profile for \(n\) men and \(n\) women · Number of Latin squares · Number of soulmate pairs

TheoremMutually Latin profiles with \(k\) soulmate pairs#●ready to prove

Let \(n\) and \(k\) be natural numbers and let \(L_n\) be the number of Latin squares of order \(n\). Call the men's preferences of a preference profile for \(n\) men and \(n\) women Latin when, for every position \(r\), distinct men rank distinct women at position \(r\), and likewise for the women's preferences. The number of preference profiles whose men's and women's preferences are both Latin and that have exactly \(k\) soulmate pairs is

\[\frac{L_n^2}{n!} \binom{n}{k} \sum_{i=0}^{n-k} \frac{(-1)^i (n-k)!}{i!}.\]

When \(k > n\) the binomial coefficient vanishes and both sides are \(0\).

public theorem_wanted mutually_latin_soulmate_profiles_card (n k : ℕ) :
    (Nat.card {P : PreferenceProfile n //
        (∀ r : Fin n, Function.Injective fun i => P.1 i r) ∧
          (∀ r : Fin n, Function.Injective fun j => P.2 j r) ∧ soulmatePairCount P = k} : ℚ) =
      (latinSquareCount n : ℚ) ^ 2 / (n ! : ℚ) * (n.choose k : ℚ) *
        ∑ i ∈ range (n - k + 1), (-1 : ℚ) ^ i * ((n - k)! : ℚ) / (i ! : ℚ)
Sources
  • Borodin et al., Sequences of the Stable Matching Problem, Journal of Integer Sequences 27 (2024), Article 24.2.2, Theorem 9 (jis-2024-24.2.2-thm-9).
Uses 3
Statement usesPreference profile for \(n\) men and \(n\) women · Number of Latin squares · Number of soulmate pairs

TheoremAt most one hell-couple in a stable matching#●ready to prove

Let \(P\) be a preference profile of \(n\) men and \(n\) women, and let \(\mu\) be a stable matching for \(P\), in which man \(i\) marries woman \(\mu(i)\). Then at most one man \(i\) forms a hell-couple with his wife \(\mu(i)\).

public theorem_wanted hellCouple_subsingleton (P : PreferenceProfile n)
    (μ : Equiv.Perm (Fin n)) (hμ : IsStableMatching P μ) :
    {i : Fin n | IsHellCouple P μ i}.Subsingleton
Sources
  • Borodin et al., Sequences of the Stable Matching Problem, Journal of Integer Sequences 27 (2024), Article 24.2.2, Proposition 12 (jis-2024-24.2.2-prop-12).
Uses 3
Statement usesHell-couple · Stable matching · Preference profile for \(n\) men and \(n\) women

TheoremA hell-couple belongs to every stable matching#●ready to prove

Let \(P\) be a preference profile for \(n\) men and \(n\) women and let \(\mu\) and \(\nu\) be stable matchings for \(P\). If man \(i\) and his wife \(\mu(i)\) form a hell-couple in \(\mu\) (each ranks the other last), then \(\nu(i) = \mu(i)\).

public theorem_wanted hellCouple_mem_all_stable (P : PreferenceProfile n)
    (μ ν : Equiv.Perm (Fin n)) (hμ : IsStableMatching P μ) (hν : IsStableMatching P ν)
    (i : Fin n) (hi : IsHellCouple P μ i) :
    ν i = μ i
Sources
  • Borodin et al., Sequences of the Stable Matching Problem, Journal of Integer Sequences 27 (2024), Article 24.2.2, Proposition 13 (jis-2024-24.2.2-prop-13).
Uses 3
Statement usesHell-couple · Stable matching · Preference profile for \(n\) men and \(n\) women

TheoremProfiles with a pair of outcasts#●ready to prove

In a preference profile for \(n\) men and \(n\) women, a man \(i\) and a woman \(j\) form a pair of outcasts when every man other than \(i\) ranks \(j\) last and every woman other than \(j\) ranks \(i\) last. The number of preference profiles with at least one pair of outcasts is \(14\) if \(n = 2\) and \(n^4 ((n-1)!)^{2n}\) if \(n \ne 2\) (this is \(0\) for \(n = 0\)).

public theorem_wanted outcast_profiles_card (n : ℕ) :
    Nat.card {P : PreferenceProfile n // ∃ i j : Fin n,
        (∀ i' : Fin n, i' ≠ i → manRank P i' j = n - 1) ∧
          (∀ j' : Fin n, j' ≠ j → womanRank P j' i = n - 1)} =
      if n = 2 then 14 else n ^ 4 * ((n - 1)!) ^ (2 * n)
Sources
  • Borodin et al., Sequences of the Stable Matching Problem, Journal of Integer Sequences 27 (2024), Article 24.2.2, Proposition 14 (jis-2024-24.2.2-prop-14).
Uses 3
Statement usesPreference profile for \(n\) men and \(n\) women · Rank of a woman for a man · A woman's rank of a man
33 fully proved11 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.