Read-back: single_parameter_characterization

Setting. $\iota$ is a finite type of agents with decidable equality (possibly empty); $A$ is an arbitrary type of outcomes (no finiteness or nonemptiness assumed). Given: a family of "winning sets" $W : \iota \to \mathcal{P}(A)$; real numbers $t_0 \le t_1$ (this inequality is an explicit hypothesis, so the interval $[t_0, t_1]$ is nonempty); an outcome rule $f : (\iota \to \mathbb{R}) \to A$ mapping real-valued type profiles to outcomes; and payments $p_i : (\iota \to \mathbb{R}) \to \mathbb{R}$. For a type profile $t : \iota \to \mathbb{R}$, say $t$ is in the box if $t_j \in [t_0, t_1]$ for every $j$; write $t[i \mapsto s]$ for $t$ with coordinate $i$ replaced by $s$ (so $t[i \mapsto t_i] = t$). Agent $i$'s valuation with type $\tau$ is the single-parameter function

i.e. $\tau$ times the indicator of the winning set $W_i$ (this is the literal unfolding used below; if $W_i = \emptyset$ it is identically $0$).

Standing hypothesis (SPNormalized W t0 t1 f p). For every profile $t$ in the box and every agent $i$: if $f(t) \notin W_i$, then $p_i(t) = 0$ — losing agents pay exactly zero at box profiles. Nothing is assumed about payments of winning agents or outside the box.

Assertion. Under that hypothesis, the following if and only if holds.

Left side — SPIncentiveCompatible W t0 t1 f p: for every profile $t$ in the box, every agent $i$, and every report $s \in [t_0, t_1]$,

Concretely: (the true type $t_i$ if the outcome under the deviated profile lies in $W_i$, else $0$) minus the payment at the deviated profile, is at most (the true type $t_i$ if the truthful outcome lies in $W_i$, else $0$) minus the payment at the truthful profile. Non-strict inequality; deviations restricted to $[t_0, t_1]$.

Right side — the conjunction of two properties:

1. SPMonotone W t0 t1 f: for every profile $t$ in the box, every agent $i$, and all $s, s' \in [t_0, t_1]$ with $s \le s'$: if $f(t[i \mapsto s]) \in W_i$ then $f(t[i \mapsto s']) \in W_i$. Winning is upward closed in one's own report, others' coordinates held fixed at $t$'s values (the original $t_i$ is overwritten and plays no role in this clause).

2. SPCriticalPayments W t0 t1 f p: for every profile $t$ in the box and every agent $i$, there exists a real $c$ (depending on $t$ and $i$) such that:

   • every winning report pays $c$: for all $s \in [t_0, t_1]$ with $f(t[i \mapsto s]) \in W_i$, one has $p_i(t[i \mapsto s]) = c$; and
   • if some report $s \in [t_0, t_1]$ loses ($f(t[i \mapsto s]) \notin W_i$), then $c$ is the least upper bound — in the IsLUB sense: an upper bound that is $\le$ every upper bound — of the set $\{ s \in [t_0, t_1] : f(t[i \mapsto s]) \notin W_i \}$. The supremum condition does not require $c$ itself to be a losing (or any) report, and no equation relates $c$ to payments at losing reports (those are $0$ by the standing hypothesis, at box profiles).

Guards and degenerate cases. If no report in $[t_0, t_1]$ loses, the IsLUB clause is vacuous and $c$ is pinned down only as the common payment of winning reports; if no report wins, the constant-payment clause is vacuous and $c$ is required only to be the least upper bound of the losing set (which is all of $[t_0, t_1]$, forcing $c = t_1$). If $\iota$ is empty, every quantified condition on both sides is vacuous and the biconditional holds trivially. If $A$ is empty, no $f$ into $A$ exists, so the statement is vacuous for lack of an $f$. All conditions on both sides are confined to profiles in the box $[t_0, t_1]^{\iota}$ and reports in $[t_0, t_1]$; the behavior of $f$ and $p$ elsewhere is unconstrained and irrelevant. The equivalence is exactly between the displayed incentive inequality and the conjunction (1) ∧ (2), given normalization; normalization itself is a hypothesis, not part of either side.