Read-back: male_propose_strategyproof

Setting. Let $M$ and $W$ be finite types, with decidable equality assumed on $M$ (needed for the pointwise profile update below); either may be empty. Profiles: $P^M$ assigns to each $m \in M$ a binary relation $P^M_m$ on $W$ (write $P^M_m(w,w')$ when the relation holds of $(w,w')$), and $P^W$ assigns to each $w \in W$ a binary relation $P^W_w$ on $M$. The theorem is about an arbitrary given function

total on all inputs (including non-profiles), with no construction (such as deferred acceptance) appearing in the statement. Note a hidden consequence of the binder itself: since relation families always exist, the mere assumption that a function $F$ into the type of bijections $M \simeq W$ exists forces that type to be nonempty, i.e. $|M| = |W|$; no explicit cardinality hypothesis is stated.

Hypothesis $h_F$. For all pairs $(P^M, P^W)$ in which every $P^M_m$ is a strict total order on $W$ and every $P^W_w$ is a strict total order on $M$ (trichotomous, irreflexive, transitive), the bijection $\mu := F(P^M, P^W)$ is male-optimal, which unfolds to the conjunction:

1. $\mu$ is stable: $\forall m\, \forall w,\ \neg\big( P^M_m(w, \mu(m)) \wedge P^W_w(m, \mu^{-1}(w)) \big)$ — no blocking pair;
2. for every bijection $\nu : M \to W$ that is stable in the same sense, and every $m \in M$: $\mu(m) = \nu(m)$ or $P^M_m\big(\mu(m), \nu(m)\big)$.

Conclusion. For every pair of profiles $(P^M, P^W)$ with all individual relations strict total orders, for every man $m \in M$, and for every strict total order $r'$ on $W$, writing $\widetilde{P}^M := P^M[m \mapsto r']$ for the men's family agreeing with $P^M$ except that $m$'s relation is replaced by $r'$:

That is: the woman $m$ is matched to when his slot carries $r'$ is the same as under the original profile; or $m$'s original relation $P^M_m$ holds of the ordered pair (partner under the original profiles, partner under the deviated profiles). The disjunction is inclusive; the comparison always uses $P^M_m$, never $r'$, which enters only through the input handed to $F$.

Points to note.

• Only men deviate, and only the men's profile is updated; the women's profile $P^W$ is held fixed throughout, and nothing whatsoever is claimed about deviations by women.
• Nothing is asserted about the partners of men other than $m$, nor about outcomes on inputs that are not strict-total-order profiles ($F$'s values there are unconstrained by both hypothesis and conclusion).
• The conclusion is the literal disjunction shown, not the formally different "$\neg\, P^M_m(\text{deviation partner}, \text{truthful partner})$".
• Degenerate cases: if $M$ and $W$ are both empty, all quantifications over $m$ are vacuous and the statement holds trivially; if exactly one is empty no $F$ of the displayed type exists, so the theorem is vacuous for such instances. If no $F$ satisfies $h_F$ (e.g. if male-optimal matchings fail to exist for some profile), the theorem is vacuously true for every such $F$; it asserts the implication for every $F$ of the displayed type satisfying $h_F$.