Read-back: house_core_unique

Setting and hypotheses. Let $N$ be a finite type with decidable equality (it may be empty). A single type plays the role of both agents and objects: each $i \in N$ carries a binary relation $P_i$ on $N$ itself (write $P_i(x, y)$ when the relation holds of the ordered pair $(x,y)$), and an "allocation" is a bijection $\sigma : N \to N$ (a Lean Equiv: a map with a two-sided inverse). The only hypothesis is

• $h_P$: for every $i \in N$, the relation $P_i$ is a strict total order on $N$ — trichotomous ($\forall x\,y$, $P_i(x,y)$ or $x = y$ or $P_i(y,x)$), irreflexive, and transitive.

Note that no initial endowment appears anywhere in the statement: nothing says agent $i$ "owns" object $i$; the indexing of objects by the agent type is the only link.

Conclusion — a unique-existence claim ($\exists!$). There exists a bijection $\sigma : N \to N$ that is unblocked, and every bijection with that property equals $\sigma$. Precisely, it asserts the conjunction:

1. Existence: some $\sigma : N \simeq N$ satisfies $\neg\,\mathrm{HouseBlocked}(P, \sigma)$;
2. Uniqueness: for every $\sigma' : N \simeq N$, if $\neg\,\mathrm{HouseBlocked}(P, \sigma')$ then $\sigma' = \sigma$. Equality here is equality of Equivs, which amounts to the two bijections agreeing as functions on every point of $N$.

Unfolding the blocking notion. $\mathrm{HouseBlocked}(P, \sigma)$ says: there exist a set $S \subseteq N$ and a bijection $\tau : N \to N$ such that

• $S$ is nonempty;
• $\tau$ maps $S$ into $S$ ($\forall i \in S,\ \tau(i) \in S$; stated as "into", though on a finite type an injective self-map of $S$ into $S$ is automatically onto $S$);
• every member weakly gains: $\forall i \in S$, $\tau(i) = \sigma(i)$ or $P_i(\tau(i), \sigma(i))$;
• at least one member strictly gains: $\exists i \in S$ with $P_i(\tau(i), \sigma(i))$.

So the theorem's object is a $\sigma$ admitting no such pair $(S, \tau)$: no nonempty coalition $S$, together with a global bijection $\tau$ keeping $S$'s assignments inside $S$, gives every member of $S$ either the same object or a $P_i$-related-above object, with the relation holding strictly for at least one member. The blocking $\tau$ is unconstrained off $S$, and $S$ may be all of $N$ — so in particular being unblocked entails there is no reallocation of everything that all agents weakly "improve" under (in the displayed sense) with one improving strictly (a Pareto-type condition as the special case $S = N$).

Edge cases. If $N$ is empty, the identity is the unique bijection $N \simeq N$, no nonempty $S$ exists so nothing is blocked, and the $\exists!$ holds trivially. If $N$ is a singleton, similarly the identity is unique and unblocked (irreflexivity kills any strict gain). The uniqueness half is a genuine assertion for larger $N$: the theorem claims there are never two distinct unblocked bijections, for any profile of strict total orders.