EconCSLib.MarketDesign.Matching.Lattice #
Building blocks for the Conway–Knuth lattice structure on the set of stable matchings of a one-to-one market (#231 item B).
This file currently contains the opposed-preferences lemma, the crux on which the lattice construction rests: across two stable matchings, whenever a man does strictly better, the woman he gains does strictly worse. It is a direct pairwise stability argument (no global counting, no lattice machinery).
The full lattice — stableJoin / stableMeet, their matching-validity and
stability, the Lattice instance and distributivity — is tracked as the
remainder of #231 item B and builds on this lemma.
References #
- [MSZ Theorem 22.12] Maschler, Solan, Zamir, Game Theory, §22.
- Knuth (1976), Mariages Stables.
- Roth & Sotomayor (1990), Ch. 2 §2.3.
Opposed preferences. Let μ be a stable matching. If man j is matched
to woman wj under another matching ν and strictly prefers wj to his
μ-partner wj', then wj strictly prefers her μ-partner m' to j.
Intuition: the two sides' interests are opposed across stable matchings — when
a man trades up, the woman he gains trades down. Proof: otherwise (wj, j)
would be a blocking pair for μ (he prefers her to his μ-partner by
hypothesis; she would prefer him to her μ-partner m'), contradicting
stability. Only μ need be stable.
Partner extraction (stable ⇒ perfect) #
The woman partnered to man j under a stable matching μ (total, since a
stable matching of the balanced market is perfect).
Equations
- GS.wPartner μ hμ j = (μ.matchW j).get ⋯
Instances For
The man partnered to woman i under a stable matching μ.
Equations
- GS.mPartner μ hμ i = (μ.matchM i).get ⋯
Instances For
The man-of and woman-of partner maps are inverse to each other.
The join (man-optimal of two) and its injectivity #
Man j's more-preferred partner across stable matchings μ and ν.
Equations
- GS.joinWoman μ ν hμ hν j = if List.idxOf (GS.wPartner μ hμ j) (m.prefs j) ≤ List.idxOf (GS.wPartner ν hν j) (m.prefs j) then GS.wPartner μ hμ j else GS.wPartner ν hν j
Instances For
If i is the join-partner of her μ-man j, then i weakly prefers her
ν-man to j (so j is her worse man).
Dual of joinWoman_worse_left with the roles of μ, ν swapped.
The join woman-assignment is injective.
Strict-preference reductions for the ofEquivData market #
The join as a stable matching #
The join woman-assignment packaged as an equivalence (injective on the
finite Fin n, hence bijective).
Equations
- GS.joinEquiv μ ν hμ hν = Equiv.ofBijective (GS.joinWoman μ ν hμ hν) ⋯
Instances For
The join μ ∨ ν: each man keeps his more-preferred of the two
partners; each woman keeps her less-preferred man.
Equations
- GS.stableJoin μ ν hμ hν = { matchM := fun (i : Fin n) => some ((GS.joinEquiv μ ν hμ hν).symm i), matchW := fun (j : Fin n) => some (GS.joinWoman μ ν hμ hν j), consistent := ⋯ }
Instances For
The join of two stable matchings is stable.
The meet (man-pessimal of two), dual to the join #
The meet μ ∧ ν gives every man his worse of the two partners, equivalently
every woman her better of the two men. We mirror the join construction over
women: meetMan (each woman's preferred man) is the relevant bijection.
Dual of opposed_preferences: if woman i strictly prefers man mi to her
candidate-man mi', then mi strictly prefers his candidate-woman to i.
Woman i's more-preferred man across μ and ν.
Equations
- GS.meetMan μ ν hμ hν i = if List.idxOf (GS.mPartner μ hμ i) (w.prefs i) ≤ List.idxOf (GS.mPartner ν hν i) (w.prefs i) then GS.mPartner μ hμ i else GS.mPartner ν hν i
Instances For
The meet man-assignment packaged as an equivalence.
Equations
- GS.meetEquiv μ ν hμ hν = Equiv.ofBijective (GS.meetMan μ ν hμ hν) ⋯
Instances For
The meet μ ∧ ν: each woman keeps her more-preferred man; each man
keeps his less-preferred woman.
Equations
- GS.stableMeet μ ν hμ hν = { matchM := fun (i : Fin n) => some (GS.meetMan μ ν hμ hν i), matchW := fun (j : Fin n) => some ((GS.meetEquiv μ ν hμ hν).symm j), consistent := ⋯ }
Instances For
The meet of two stable matchings is stable.
Order-theoretic characterizations of join and meet #
The meet woman of man j is one of his two partners (his worse).
The lattice of stable matchings #
The type of stable matchings of a one-to-one market.
Equations
- GS.StableMatching w' m' = { μ : Matching (Fin n) (Fin n) // Matching.IsStable (MatchingMarket.ofEquivData w' m') μ }
Instances For
Man j's partner under a stable matching.
Equations
- μ.partner j = GS.wPartner ↑μ ⋯ j
Instances For
Men-preference order: μ ≤ ν iff every man weakly prefers his ν-partner
to his μ-partner (smaller idxOf = more preferred).
Equations
- One or more equations did not get rendered due to their size.
Conway–Knuth lattice. The stable matchings of a one-to-one market form a lattice under the men-preference order: the join gives every man his more- preferred of two partners, the meet his less-preferred, and both are stable.
Equations
- One or more equations did not get rendered due to their size.
Men-optimality as the lattice maximum #
The men-proposing Gale–Shapley output, as an element of the lattice of stable matchings.
Equations
- GS.StableMatching.gsStable w' m' = ⟨Matching.ofGS (GS.gs w' m') ⋯, ⋯⟩
Instances For
The GS output is the greatest stable matching in the men-preference
order: every man weakly prefers his GS partner to his partner in any other
stable matching. This is galeShapley_isProposingOptimal packaged as the
lattice maximum (⊤-like greatest element).
gsStable is the greatest element of the stable-matching lattice.