Strategyproof.lean

View source on GitHub

The four cases

The proof splits on two binary questions: does player i win when truthful? Does player i win when deviating? That gives four cases:

Case 1: both win

Utility = trueVal_i - C in both cases, where C = welfareOthersWithout. By welfareOthersWithout_invariant, C doesn't depend on i's report. So utility is identical.

Case 2: truth wins, deviation loses

Truthful utility = trueVal_i - C ≥ 0 by welfareOthersWithout_le_trueVal_of_win: winning truthfully means your value exceeds the externality. Deviated utility = 0 by playerUtility_eq_zero_of_loser. Truth wins.

Case 3: truth loses, deviation wins

Truthful utility = 0. Deviated utility = trueVal_i - C ≤ 0 by trueVal_le_welfareOthersWithout_of_loss: losing truthfully means the externality exceeds your value, and C is invariant. Truth wins again.

Case 4: both lose

Both utilities are 0 by playerUtility_eq_zero_of_loser.

welfareOthersWithout_invariant (payment invariance)

Changing player i's report does not change welfareOthersWithout. The counterfactual welfare with i removed depends only on other players' reports. This is the structural property that makes VCG dominant-strategy rather than just Nash.

theorem welfareOthersWithout_invariant
    (auc : Auction ι E) (i : ι) (r' : Report E) (x : E) :
    welfareOthersWithout (auc.withReport i r') i x =
      welfareOthersWithout auc i x

vcg_dsic

The main result. For any deviation r' that player i might submit, truthful utility ≥ deviated utility. The hypothesis is isTruthful (auc.report i) (auc.valuation i) — only player i needs to be truthful. Others can report anything.

theorem vcg_dsic
    (auc : Auction ι E) (i : ι) (x : E) (r' : Report E)
    (hi : isTruthful (auc.report i) (auc.valuation i)) :
    playerUtility auc i x ≥
      playerUtility (auc.withReport i r') i x

Vickrey (1961) Thm 1, Clarke (1971) §3, Groves (1973) Thm 2. This is the machine-checked version of the DSIC claim in Vector Space.

; DSIC: no bid beats truthful
(define (score c s bid x)
  (- (log bid) (/ (* (- x c) (- x c)) (* s s))))

(define (trueVal c s v x)
  (* v (exp (- (/ (* (- x c) (- x c)) (* s s))))))

(define (reportedVal c s bid x)
  (* bid (exp (- (/ (* (- x c) (- x c)) (* s s))))))

(define ic 0.5) (define is 0.3) (define iv 4.0)
(define oc 0.4) (define os 0.25) (define ob 3.5)
(define x 0.45)

(define (wins? bid)
  (>= (score ic is bid x) (score oc os ob x)))

(define (utility bid)
  (if (wins? bid)
      (- (trueVal ic is iv x) (reportedVal oc os ob x))
      0.0))

(define truth iv)
(define ut (utility truth))

(for-each (lambda (lie)
  (let ((ul (utility lie)))
    (display lie) (display "  ")
    (display (wins? lie)) (display "  u=")
    (display (round (* ul 1000))) (display "/1000  truth>=lie: ")
    (display (>= (+ ut 1e-10) ul)) (newline)))
  '(0.5 1.0 2.0 4.0 6.0 10.0 20.0))

import math

def score(c, s, bid, x):
    return math.log(bid) - (x - c)**2 / s**2

def trueVal(c, s, v, x):
    return v * math.exp(-(x - c)**2 / s**2)

def reportedVal(c, s, bid, x):
    return bid * math.exp(-(x - c)**2 / s**2)

# Player i and one other
i = {"c": 0.5, "s": 0.3, "v": 4.0}
other = {"c": 0.4, "s": 0.25, "bid": 3.5}
x = 0.45

def wins(bid):
    return score(i["c"], i["s"], bid, x) >= score(other["c"], other["s"], other["bid"], x)

def utility(bid):
    tv = trueVal(i["c"], i["s"], i["v"], x)
    C = reportedVal(other["c"], other["s"], other["bid"], x)
    return (tv - C) if wins(bid) else 0.0

truth = i["v"]
ut = utility(truth)
tw = wins(truth)

print(f"{'bid':>6} {'wins':>5} {'utility':>8} {'truth>=lie':>10}")
for lie in [0.5, 1.0, 2.0, 4.0, 6.0, 10.0, 20.0]:
    ul = utility(lie)
    lw = wins(lie)
    tag = "TRUTH" if lie == truth else ""
    print(f"{lie:6.1f} {str(lw):>5} {ul:8.3f} {str(ut >= ul - 1e-10):>10}  {tag}")

Corollaries

vcg_strategyproof: when all players are truthful, no single player benefits from deviating. (DSIC implies Nash.)

vcg_is_nash_equilibrium: truthful reporting satisfies the open-game Nash equilibrium condition from OpenGame.lean.

truthful_sigma_is_best_response: even if a player only deviates in sigma (keeping center and bid fixed), truthful sigma is still optimal.

Connections

• Efficiency.lean — supplies winner_maximizes_reportedVal and reportedVal_eq_trueVal_of_truthful
• OpenGame.lean — the vcg_is_nash_equilibrium corollary connects to Hedges' framework
• GaussianOptimality.lean — bundles strategyproofness with welfare-optimality in the capstone
• Vickrey (1961) — counterspeculation, auctions, and competitive sealed tenders
• Clarke (1971) — multipart pricing of public goods
• Groves (1973) — incentives in teams