Claim 5.2, proof — the utility of an agent equals its bonus

Proved

AlgMechDesign.CompBonus.cb_utility_eq_bonus

by mikedeng1 · Sep 28, 2026 · Mathlib 0df444a (Lean v4.33.1)

mechanism-designp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1scheduling

Consider the Compensation-and-Bonus payments $p^i = c^i + b^i$ built on an arbitrary allocation rule $x(\cdot)$ . Let $d$ be any declaration profile and let every agent follow any execution plan, producing actual times $\tilde t$ . Then the utility of every agent $i$ equals its bonus:

p^i(d,\tilde t) - \sum_{j \in x^i(d)} \tilde t_j \;=\; b^i(d, \tilde t) \;=\; -g\big(x(d), \mathrm{corr}^i(x(d), d, \tilde t)\big).

The compensation exactly reimburses the agent's actual work, so its incentives are driven by the bonus alone. This is the first observation of the proof of Claim 5.2.

Preamble

import Mathlib
import Definitions.Def_AlgMechDesign_CompBonus_Model
import Definitions.Def_AlgMechDesign_CompBonus_Mechanism

Formal statement

namespace AlgMechDesign.CompBonus

/-- Proof of Claim 5.2 (p. 188): in the Compensation-and-Bonus mechanism based on any allocation
algorithm, the utility of agent `i` (payment plus valuation) equals its bonus, for all
declarations `d` and all execution plans `E`. -/
theorem cb_utility_eq_bonus {n k : ℕ} [NeZero n]
    (alloc : (Fin n → Fin k → ℝ) → (Fin k → Fin n)) (d : Fin n → Fin k → ℝ)
    (E : Fin n → ExecPlan n k) (i : Fin n) :
    utility alloc (cbPay alloc) d E i = bonus alloc d (actualTimes alloc d E) i := by sorry

end AlgMechDesign.CompBonus

Source

Nisan, Ronen, Algorithmic Mechanism Design, Games Econ. Behav. 35, 2001, p. 188, proof of Claim 5.2, first paragraph, third sentence ("Observing that the utility of an agent equals its bonus, …")

Human review

Endorsed by Shuze Chen · Oct 1, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph