Read-back: ttc_strategyproof

Setting. Let $N$ be a finite type with decidable equality (possibly empty). A "profile" assigns to each $i \in N$ a binary relation on $N$ (write $P_i(x,y)$ when $i$'s relation holds of the ordered pair $(x,y)$); an "allocation" is a bijection $N \to N$ (a Lean Equiv). The theorem is about an arbitrary given function

$F$ is total: it is defined on every family of relations, including families that are not preference profiles; no construction of $F$ (such as a top-trading-cycles algorithm) appears in the statement — $F$ is characterized only by the hypothesis below.

Hypothesis $h_F$. For every profile $P$ such that each $P_i$ is a strict total order on $N$ (trichotomous, irreflexive, transitive), the allocation $F(P)$ is unblocked — unfolding the custom predicate HouseBlocked, this means: there do not exist a nonempty set $S \subseteq N$ and a bijection $\tau : N \to N$ with $\tau(S) \subseteq S$, such that every $i \in S$ has $\tau(i) = F(P)(i)$ or $P_i\big(\tau(i), F(P)(i)\big)$, and at least one $i \in S$ has $P_i\big(\tau(i), F(P)(i)\big)$. (Only pref profiles are constrained; $F$'s values on other inputs are arbitrary.)

Conclusion. For every profile $P$ with each $P_i$ a strict total order, for every agent $i \in N$, and for every binary relation $r'$ on $N$ that is a strict total order, letting $P' := P[i \mapsto r']$ denote the profile that agrees with $P$ at every agent except $i$, where the relation is replaced by $r'$:

That is: the object agent $i$ receives when the profile carries $r'$ in $i$'s slot equals the object $i$ receives under $P$; or $i$'s original relation $P_i$ holds of the ordered pair (object under $P$, object under $P'$). The disjunction is inclusive. The comparison always uses $P_i$, never $r'$; $r'$ enters only through the deviated profile $P'$ handed to $F$.

Points to note.

• The quantifier order is: profile $P$ first, then agent $i$ and alternative relation $r'$ — so the claim covers every unilateral replacement at every agent of every strict-total-order profile.
• The conclusion is the literal disjunction displayed above, not the (formally different) statement "$\neg\, P_i\big(F(P')(i), F(P)(i)\big)$"; the exact form asserted is equal outcome or truthful outcome $P_i$-related above the deviation outcome.
• Nothing constrains what happens to agents other than $i$ under $P'$, and nothing is asserted for relations $r'$ that fail to be strict total orders, nor for base profiles $P$ that fail to be preference profiles.
• Degenerate cases: if $N$ is empty, the conclusion quantifies over no agents and holds vacuously (and $h_F$ is about the unique empty bijection, unblocked because no nonempty $S$ exists). If $h_F$ is unsatisfiable for a given $F$, the theorem holds vacuously for that $F$; the statement asserts the implication for every $F$ of the displayed type.