Efficiency.lean

View source on GitHub

isTruthful / allTruthful

A report is truthful when it matches the player's private valuation: same center, same sigma, bid equals true value. allTruthful extends this to every player.

def isTruthful (r : Report E) (v : Valuation E) : Prop :=
  r.center = v.center ∧ r.sigma = v.trueSigma ∧ r.bid = v.trueValue

score_eq_log_trueVal (Bridge 1: truthful)

Under truthful reporting, score_i(x) = log(trueVal_i(x)). The scoring function is the log of the value function when reports are honest. Since log is monotone, maximizing score is the same as maximizing value.

theorem score_eq_log_trueVal (r : Report E) (v : Valuation E) (x : E)
    (h : isTruthful r v) :
    score r x = Real.log (trueVal v x)

The proof: substitute the truthful equalities into the score definition, use log(a · exp(b)) = log(a) + b from Mathlib. Pure algebra.

score_eq_log_reportedVal (Bridge 2: unconditional)

score = log(reportedVal) always — no truthfulness needed. The mechanism always maximizes reported welfare. Only the truthful player aligns reported with true welfare. This is the key to DSIC.

theorem score_eq_log_reportedVal (r : Report E) (x : E) :
    score r x = Real.log (reportedVal r x)

; Bridge 1 vs Bridge 2
(define center 0.4) (define sigma 0.3) (define value 7.0)
(define x 0.6)

(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))))))

; Bridge 1: truthful => score = log(trueVal)
(let ((s (score center sigma value x))
      (tv (log (trueVal center sigma value x))))
  (display "Truthful: score=") (display s)
  (display " log(trueVal)=") (display tv)
  (display " match=") (display (< (abs (- s tv)) 1e-10))
  (newline))

; Lie: bid = 20
(let ((s (score center sigma 20.0 x))
      (tv (log (trueVal center sigma value x))))
  (display "Lying:    score=") (display s)
  (display " log(trueVal)=") (display tv)
  (display " match=") (display (< (abs (- s tv)) 1e-10))
  (newline))

; Bridge 2: always holds
(let ((s (score center sigma 20.0 x))
      (rv (log (reportedVal center sigma 20.0 x))))
  (display "Bridge 2: score=") (display s)
  (display " log(rVal)=") (display rv)
  (display " match=") (display (< (abs (- s rv)) 1e-10))
  (newline))

import math

center, sigma, value = 0.4, 0.3, 7.0
x = 0.6

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)

# Bridge 1: truthful => score = log(trueVal)
s1 = score(center, sigma, value, x)
tv = trueVal(center, sigma, value, x)
print(f"Truthful:  score = {s1:.6f}")
print(f"           log(trueVal) = {math.log(tv):.6f}")
print(f"           match = {abs(s1 - math.log(tv)) < 1e-10}")

# Lie: inflate bid to 20
s2 = score(center, sigma, 20.0, x)
print(f"\nLying bid: score = {s2:.6f}")
print(f"           log(trueVal) = {math.log(tv):.6f}")
print(f"           match = {abs(s2 - math.log(tv)) < 1e-10}")

# Bridge 2: score = log(reportedVal) always
rv = reportedVal(center, sigma, 20.0, x)
print(f"\nBridge 2:  score = {s2:.6f}")
print(f"           log(reportedVal) = {math.log(rv):.6f}")
print(f"           match = {abs(s2 - math.log(rv)) < 1e-10}")

winner_maximizes_reportedVal

For any player j, the winner's reported value is at least j's reported value. Follows from Bridge 2 plus the argmax definition of winner. No truthfulness required.

theorem winner_maximizes_reportedVal (auc : Auction ι E) (x : E) (j : ι) :
    reportedVal (auc.report (winner auc x)) x ≥
      reportedVal (auc.report j) x

winner_maximizes_welfare

Under truthful reporting, the winner at each query point achieves the highest true value among all players. This is the pointwise welfare-maximization result. The proof chain: argmax of score → argmax of log(trueVal) via Bridge 1 → argmax of trueVal by monotonicity of log.

theorem winner_maximizes_welfare (auc : Auction ι E) (x : E)
    (htruth : allTruthful auc) (j : ι) :
    trueVal (auc.valuation (winner auc x)) x ≥
      trueVal (auc.valuation j) x

This is the result that lifts to integrated welfare in IntegralEfficiency.lean.

Connections

• Auction.lean — defines score, trueVal, reportedVal, winner
• Strategyproof.lean — uses winner_maximizes_reportedVal for the DSIC proof
• IntegralEfficiency.lean — lifts winner_maximizes_welfare to integrals