Read-back: ic_iff_monotone

Setting. Let $A$ and $\iota$ be arbitrary types ($A$ the "alternatives", $\iota$ the "individuals"), with equality on $\iota$ decidable. A profile is a family $P$ assigning to each $i \in \iota$ a binary relation $P_i$ on $A$; the profile is called admissible (the bundle's IsPrefProfile) when every $P_i$ is a strict total order on $A$, i.e. irreflexive, transitive, and trichotomous (for all $x, y$: $P_i\,x\,y$, or $x = y$, or $P_i\,y\,x$). For a profile $P$, an individual $i$, and a relation $r'$, write $P[i \mapsto r']$ for the profile that agrees with $P$ at every coordinate except $i$, where it is $r'$.

The theorem. For every function $f$ mapping profiles (arbitrary families of binary relations on $A$, admissible or not) to single alternatives in $A$, the following two properties of $f$ are equivalent (a genuine biconditional — each side implies the other):

Left side (IncentiveCompatible f). For every admissible profile $P$, every individual $i$, and every strict total order $r'$ on $A$: it is not the case that the relation $P_i$ holds of the pair

that is, $P_i$ does not relate the outcome of the modified profile (first argument) to the outcome of the original profile (second argument). Only the truthful relation $P_i$ appears in the conclusion; $r'$ enters only through the modified profile.

Right side (SCFMonotone f). For every admissible profile $P$, every individual $i$, and every strict total order $r'$ on $A$: if the two outcomes differ, $f(P) \neq f(P[i \mapsto r'])$, then both of the following hold:

i.e. the original relation $P_i$ relates the original outcome (first argument) to the modified outcome (second argument), and the replacement relation $r'$ relates the modified outcome (first argument) to the original outcome (second argument) — the two conclusions point in opposite orientations. When $f(P) = f(P[i \mapsto r'])$ this side imposes no condition at all for that $(P, i, r')$.

Quantifier fine print.

• On both sides, $r'$ ranges over all strict total orders on $A$, including $r' = P_i$ itself; nothing requires the deviation to actually change $i$'s relation.
• There are no further hypotheses on $f$: it need not send admissible profiles to any distinguished alternative, need not be onto, and its values on inadmissible profiles are unconstrained (both properties only ever evaluate $f$ at admissible profiles, since replacing one coordinate of an admissible profile by a strict total order yields an admissible profile).
• If $\iota$ is empty, the quantification over $i$ on both sides is vacuous, so both properties hold trivially and the equivalence is trivially true. Likewise, if $A$ has at most one element, irreflexivity of $P_i$ and $r'$ makes both sides hold vacuously.
• The equivalence is asserted for every such $f$ individually; nothing existential is claimed.