Prove2Me

Proposition 4.4 (Independence) — the payment depends only on the allocation and t−it^{-i}

Proved
AlgMechDesign.Additive.independence

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

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

Let m=(x,p)m=(x,p) be a truthful mechanism for task scheduling, let t1t_1 and t2t_2 be positive type vectors and let ii be an agent. If t1t_1 and t2t_2 agree on every agent other than ii, i.e. t1−i=t2−it_1^{-i} = t_2^{-i}, and the mechanism gives agent ii the same set of tasks under both, xi(t1)=xi(t2)x^i(t_1) = x^i(t_2), then

pi(t1)=pi(t2).p^i(t_1) = p^i(t_2).

The payment offered to an agent therefore does not depend on its own declaration once the others' declarations and its allocation are fixed; this is what makes the prices pi(X,t−i)p^i(X,t^{-i}) of Definition 12 well defined.

Preamble
import Mathlib
import Definitions.Def_AlgMechDesign_Additive_Model
import Definitions.Def_AlgMechDesign_Additive_Price
Formal statement
namespace AlgMechDesign.Additive

/-- Proposition 4.4 (Independence), p. 177: for a truthful mechanism, if two positive type
vectors agree off agent `i` and give agent `i` the same set of tasks, then agent `i` is paid
the same amount. -/
theorem independence {n k : ℕ} (alloc : (Fin n → Fin k → ℝ) → (Fin k → Fin n))
    (pay : (Fin n → Fin k → ℝ) → Fin n → ℝ) (htr : IsTruthful alloc pay)
    (t₁ t₂ : Fin n → Fin k → ℝ) (h₁ : IsType t₁) (h₂ : IsType t₂) (i : Fin n)
    (hoth : ∀ i' : Fin n, i' ≠ i → t₁ i' = t₂ i')
    (hx : taskSet (alloc t₁) i = taskSet (alloc t₂) i) :
    pay t₁ i = pay t₂ i := by sorry

end AlgMechDesign.Additive
Source
Nisan, Ronen, Algorithmic Mechanism Design, Games Econ. Behav. 35, 2001, p. 177, Proposition 4.4 (Independence)
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