Clarke pivot payments: no positive transfers, individual rationality

Proved

AGT.clarke_pivot_properties

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

auctionsgame-theorymechanism-design

The Clarke pivot rule makes no positive transfers, and is individually rational when valuations are nonnegative (Lemma 9.20 of Algorithmic Game Theory). Let $f$ be any welfare-maximizing choice rule on the domain, and charge each player the Clarke payment $p_i(v) = \max_b \sum_{j\ne i} v_j(b) - \sum_{j\ne i} v_j(f(v))$ — the externality they impose on the others. Then:

no player is ever paid money: $p_i(v) \ge 0$ on every profile of the domain;
if every valuation in every domain is pointwise nonnegative, every player's utility $v_i(f(v)) - p_i(v)$ is nonnegative on every profile of the domain.

A note on the hypotheses. $A$ is finite and nonempty so the Clarke maximum is attained (Finset.sup'); combined with Theorem 9.17 this yields the standard "VCG with Clarke pivot" mechanism: truthful, individually rational, and never subsidizing.

Preamble

import Definitions.Def_agt_mechanism

Formal statement

namespace AGT

/-- The Clarke pivot rule makes no positive transfers, and is individually
rational when valuations are nonnegative (Lemma 9.20 of *Algorithmic Game
Theory*).  `f` is any welfare-maximizing choice rule on the domain `V`;
with the Clarke payments `pᵢ = max_b ∑_{j≠i} vⱼ(b) − ∑_{j≠i} vⱼ(f(v))`,
every payment is nonnegative, and if every valuation in every domain is
pointwise nonnegative then every player's utility is nonnegative as well.
Finiteness and nonemptiness of `A` make the Clarke maximum attained. -/
theorem clarke_pivot_properties {A ι : Type*} [Fintype ι] [DecidableEq ι]
    [Fintype A] [Nonempty A] (V : ι → Set (A → ℝ))
    (f : (ι → A → ℝ) → A) (hf : MaximizesWelfare V f) :
    NoPositiveTransfers V f (clarkePayment f) ∧
      ((∀ i, ∀ vi ∈ V i, ∀ a, 0 ≤ vi a) →
        IndividuallyRational V f (clarkePayment 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.3.4, Lemma 9.20, pp. 219-220

Read-back

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

Read-back: `clarke_pivot_properties`

Setting. $\iota$ is a finite type of agents with decidable equality (possibly empty); $A$ is a finite and nonempty type of outcomes. We are given a family $V : \iota \to \mathcal{P}(A \to \mathbb{R})$ of admissible valuation sets and an outcome rule $f : (\iota \to (A \to \mathbb{R})) \to A$ . Call a profile $v : \iota \to (A \to \mathbb{R})$ valid if $v_j \in V_j$ for all $j$ . The payment scheme in the conclusion is not a variable of the theorem: it is the concrete clarkePayment f, defined for each agent $i$ and every profile $v$ (valid or not) by

\mathrm{clarke}_i(v) \;=\; \max_{b \in A} \sum_{j \ne i} v_j(b) \;-\; \sum_{j \ne i} v_j\big(f(v)\big),

where the maximum is a genuinely attained maximum over the finite nonempty outcome set $A$ , and both sums run over all agents other than $i$ . When $\iota$ has one element both sums are empty and $\mathrm{clarke}_i(v) = 0 - 0 = 0$ .

Hypothesis. MaximizesWelfare V f: for every valid profile $v$ and every outcome $a \in A$ ,

\sum_{i \in \iota} v_i(a) \;\le\; \sum_{i \in \iota} v_i\big(f(v)\big).

This is the only assumption on $f$ ; no incentive property of $f$ or of any payments is assumed, and nothing at all is assumed about $f$ on invalid profiles.

Conclusion. The conjunction of two claims:

NoPositiveTransfers V f (clarkePayment f) (a property that, by its definition, ignores its $f$ -rule argument and constrains only the payments): for every valid profile $v$ and every agent $i$ ,

0 \;\le\; \max_{b \in A} \sum_{j \ne i} v_j(b) - \sum_{j \ne i} v_j\big(f(v)\big),

i.e. the Clarke payment of every agent is nonnegative at every valid profile. (Literally a nonnegativity claim about $\mathrm{clarke}_i(v)$ ; despite the name, no other notion of "transfer" appears.)

A conditional individual-rationality claim. If every admissible valuation is pointwise nonnegative — that is, for every agent $i$ , every $v_i' \in V_i$ , and every outcome $a \in A$ , $0 \le v_i'(a)$ — then IndividuallyRational V f (clarkePayment f) holds: for every valid profile $v$ and every agent $i$ ,

0 \;\le\; v_i\big(f(v)\big) - \Big(\max_{b \in A} \sum_{j \ne i} v_j(b) - \sum_{j \ne i} v_j\big(f(v)\big)\Big),

i.e. each agent's value for the chosen outcome minus their Clarke payment is nonnegative, at every valid profile. The nonnegativity hypothesis quantifies over all members of every $V_i$ and all outcomes, not only over the coordinates of some particular profile.

Degenerate cases the quantifiers include. If $\iota$ is empty, or some $V_j$ is empty (so there are no valid profiles), both conclusions hold vacuously, and the welfare hypothesis is likewise vacuous. If some $V_i$ is empty, the nonnegativity hypothesis of clause 2 is also vacuously satisfiable for that agent. Both conclusions are stated only at valid profiles and only with the specific Clarke payments displayed above; no incentive-compatibility statement is made anywhere in this theorem, and clause 2 is an implication only (nothing is claimed when some admissible valuation takes a negative value).

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

Clarke pivot payments: no positive transfers, individual rationality

Read-back: clarke_pivot_properties

Read-back: `clarke_pivot_properties`