Incentive compatibility forces weak monotonicity

Proved

AGT.ic_implies_wmon

by Shuze Chen · Sep 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

auctionsgame-theorymechanism-design

Incentive compatibility forces weak monotonicity of the choice rule (Theorem 9.29 of Algorithmic Game Theory, necessity half). If some payment functions make $(f, p)$ incentive compatible on the domain $V$ , then $f$ satisfies WMON: whenever a unilateral change of player $i$ 's valuation from $v_i$ to $v_i'$ moves the outcome from $a$ to $b \ne a$ , we have $v_i'(b) - v_i'(a) \ge v_i(b) - v_i(a)$ .

A note on the rendering. This half of Theorem 9.29 carries no hypotheses beyond incentive compatibility itself — no convexity, no finiteness, arbitrary domains; the book's proof is two applications of the truthfulness inequality. The sufficiency half, which does need convex domains, is the separate milestone wmon_implies_ic_convex; splitting the two keeps this direction at its full strength.

Preamble

import Definitions.Def_agt_mechanism

Formal statement

namespace AGT

/-- Incentive compatibility forces weak monotonicity of the choice rule
(Theorem 9.29 of *Algorithmic Game Theory*, necessity half): if some
payments make `f` incentive compatible, then whenever a unilateral change
of valuation moves the outcome from `a` to `b`, the deviator raised the
value of `b` relative to `a`.  This half needs no structure whatsoever on
the domains. -/
theorem ic_implies_wmon {A ι : Type*} [Fintype ι] [DecidableEq ι]
    (V : ι → Set (A → ℝ)) (f : (ι → A → ℝ) → A)
    (p : ι → (ι → A → ℝ) → ℝ) (hic : MechIncentiveCompatible V f p) :
    WeakMonotone V f := by
  sorry

end AGT

Source

N. Nisan, T. Roughgarden, E. Tardos, V. V. Vazirani (eds.), Algorithmic Game Theory, Cambridge University Press 2007, https://doi.org/10.1017/CBO9780511800481, Section 9.5.3, Theorem 9.29 (necessity), pp. 226-227

Read-back

What the Lean code literally says, in plain math · claude-fable-5

Read-back: `ic_implies_wmon`

Setting. $A$ is an arbitrary type of outcomes (no finiteness or nonemptiness assumed) and $\iota$ is a finite type of agents with decidable equality (possibly empty). Given: a family $V : \iota \to \mathcal{P}(A \to \mathbb{R})$ of admissible valuation sets, an outcome rule $f : (\iota \to (A \to \mathbb{R})) \to A$ defined on all profiles, and payments $p_i : (\iota \to (A \to \mathbb{R})) \to \mathbb{R}$ for each agent. A profile $v$ is valid if $v_j \in V_j$ for every $j$ ; $v[i \mapsto v']$ denotes $v$ with coordinate $i$ replaced by $v'$ .

Hypothesis (MechIncentiveCompatible V f p, unfolded). For every valid profile $v$ , every agent $i$ , and every $v' \in V_i$ ,

v_i\big(f(v[i \mapsto v'])\big) - p_i\big(v[i \mapsto v']\big) \;\le\; v_i\big(f(v)\big) - p_i\big(v\big):

no agent with a valid true profile can strictly increase their quasilinear utility (value of the chosen outcome under their original valuation $v_i$ , minus payment) by unilaterally deviating to any admissible valuation $v' \in V_i$ . The inequality is non-strict.

Conclusion (WeakMonotone V f, unfolded). For every valid profile $v$ , every agent $i$ , and every $v' \in V_i$ : if the outcome changes, $f(v) \ne f(v[i \mapsto v'])$ , then

v_i\big(f(v[i \mapsto v'])\big) - v_i\big(f(v)\big) \;\le\; v'\big(f(v[i \mapsto v'])\big) - v'\big(f(v)\big).

In words: writing $a = f(v)$ for the old outcome and $b = f(v[i \mapsto v'])$ for the new one, whenever $a \ne b$ , the increment $b$ -value-minus- $a$ -value is at least as large under the new valuation $v'$ as under the old valuation $v_i$ ; equivalently $v_i(b) - v_i(a) \le v'(b) - v'(a)$ . No condition is imposed when the outcome does not change, and payments do not appear in the conclusion at all.

Shape and degenerate cases. The theorem is a one-directional implication: from the incentive-compatibility of the pair $(f, p)$ for this particular given $p$ , it concludes the payment-free monotonicity property of $f$ alone. If $\iota$ is empty, or some $V_j$ is empty (so no valid profile exists), both hypothesis and conclusion hold vacuously. If $A$ is empty, no $f$ into $A$ exists (its domain is always inhabited), so the statement is vacuous for lack of an $f$ . Both properties quantify deviations only over $V_i$ , so a singleton $V_i$ (only one admissible valuation) makes the outcome-change guard $f(v) \ne f(v[i \mapsto v'])$ unsatisfiable for that agent, since $v[i \mapsto v_i] = v$ .

Human review

Endorsed by Community (Bot) · Sep 13, 2026
Endorsed by Shuze Chen · Sep 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Incentive compatibility forces weak monotonicity

Read-back: ic_implies_wmon

Read-back: `ic_implies_wmon`