Read-back: stable_iff_core

Setting and hypotheses. Let $M$ and $W$ be two arbitrary types — unlike the existence theorems in this bundle, no finiteness is assumed here, and neither is any cardinality hypothesis: instead a particular bijection is handed in directly. The data are:

• $P^M$ assigning to each $m \in M$ a binary relation $P^M_m$ on $W$, and $P^W$ assigning to each $w \in W$ a binary relation $P^W_w$ on $M$ (write $P^M_m(w,w')$, resp. $P^W_w(m,m')$, when the relation holds of that ordered pair);
• $h_M$: every $P^M_m$ is a strict total order on $W$ (trichotomous, irreflexive, transitive), and $h_W$: every $P^W_w$ is a strict total order on $M$;
• a given bijection $\mu : M \to W$ (an Equiv, with inverse $\mu^{-1}$). Note that supplying $\mu$ itself presupposes $M$ and $W$ are equipotent for the instance to be non-degenerate.

Conclusion (an if-and-only-if). The following two statements are equivalent.

Left side — $\mu$ is a stable matching (unfolding IsStableMatching and IsBlockingPair):

i.e. there is no pair $(m,w)$ with $m$'s relation holding of $(w, \mu(m))$ and $w$'s relation holding of $(m, \mu^{-1}(w))$.

Right side — $\mu$ is not dominated (the negation of MatchDominated): it is not the case that there exist a bijection $\nu : M \to W$ and a set $S \subseteq M$ of men such that

1. $S$ is nonempty,
2. for every $m \in S$: $P^M_m\big(\nu(m),\ \mu(m)\big)$ — each coalition man's relation holds of (his $\nu$-partner, his $\mu$-partner), and
3. for every $m \in S$: $P^W_{\nu(m)}\big(m,\ \mu^{-1}(\nu(m))\big)$ — the relation of woman $\nu(m)$ holds of ($m$, the man she was matched to under $\mu$).

Features to note in the domination notion. The coalition $S$ contains men only; the women involved are implicitly $\nu(S)$. The deviating $\nu$ must be a globally defined bijection of all of $M$ onto all of $W$, but its behavior outside $S$ is completely unconstrained — agents off the coalition may be reassigned arbitrarily and their preferences play no role. There is no closure requirement relating $\nu(S)$ to $\mu(S)$: coalition men may claim women who were matched under $\mu$ to men outside $S$. Both improvement conditions are required of all members of $S$ (there is no "weak improvement for all, strict for at least one" structure; every $m \in S$ must have the displayed relations hold outright, which under irreflexivity of $P^M_m$ forces $\nu(m) \neq \mu(m)$ for all $m \in S$).

Edge cases. If $M$ (hence $W$) is empty, the left side is vacuously true and the right side is true because no nonempty $S \subseteq M$ exists — the equivalence holds degenerately. The statement is a biconditional for the given $\mu$, quantified over nothing further: it asserts both that stability precludes such a dominating pair $(\nu, S)$ and, conversely, that absence of any such pair implies no blocking pair exists.