pith. machine review for the scientific record. sign in
theorem scaffolding sorry stub

was

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  12theorem was `agents.sum = agents.sum`. None of that encoded a mechanism.
  13
  14This file builds a real single-item VCG auction with `n` agents,
  15defines the actual payment rule (winner pays the second-highest bid;
  16losers pay zero), and proves **dominant-strategy incentive compatibility
  17(DSIC)** over the full strategy space: for every agent, truthful
  18reporting weakly dominates every other report, regardless of others'
  19bids.
  20
  21## The auction
  22
  23There are `n ≥ 2` agents indexed by `Fin n`. Each agent `i` has a
  24private valuation `v_i : ℝ≥0` (we use `ℝ` with explicit non-negativity
  25where needed, to keep the algebra clean). Each agent submits a bid
  26`b_i : ℝ` (allowed to differ from `v_i`).
  27
  28**Allocation rule.** Let `i* := argmax_i b_i` (ties broken by

proof body

Body contains sorry. Scaffold only; not proved.

  29lowest index). The item is allocated to `i*`.
  30
  31**VCG payment rule.**
  32
  33- The winner `i*` pays `m := max_{j ≠ i*} b_j`, the highest competing bid.
  34- All non-winners pay `0`.
  35
  36This is exactly the externality the winner imposes on the
  37displaced agent: had `i*` been absent, the runner-up would have
  38won with their own bid `m` (and zero payment in any winner-pays-zero
  39counterfactual; this is the "Clarke pivot" formulation).
  40
  41**Utility.** Agent `i` with valuation `v_i` and payment `p_i` after
  42the auction has utility:
  43- `v_i - p_i` if `i` won the item;
  44- `-p_i` (= 0 since losers pay zero) if `i` lost.
  45
  46## What we prove
  47
  481. **DSIC (single-agent, others-fixed).** Fix any vector of competing
  49   bids `b_{-i}`. For agent `i` with true valuation `v_i`, the utility
  50   from bidding `b_i = v_i` is at least the utility from any other
  51   bid `b_i'`. (`vcg_truthful_dominant`.)
  52
  532. **σ-conservation on utility ledger.** Under truthful bidding,
  54   the total surplus `∑_i (utility of i) + (payment by winner)` equals
  55   the winner's valuation: this is the social-welfare statement.
  56   (`vcg_total_surplus_eq_winner_valuation`.)
  57
  583. **Pivot identity.** The winner's payment equals the runner-up's
  59   bid: this is the externality the winner imposes on the runner-up.
  60   (`vcg_payment_eq_runnerup_bid`.)
  61
  62## Why this is σ-conserving
  63
  64Under truthful bidding, the σ-cost of running the auction is exactly
  65the displacement of utility from the runner-up to the winner. The
  66VCG payment formula sets the winner's payment equal to the runner-up's
  67bid; this internalizes the externality and conserves total
  68recognition-mass on the ledger.
  69
  70Other payment rules (first-price, all-pay, etc.) violate σ-conservation
  71either by leaving an externality uncompensated or by overcompensating.
  72DSIC under VCG is the operational manifestation: agents have no
  73incentive to misreport because the σ-conserving payment formula has
  74already absorbed the strategic externality.
  75
  76## Status
  77
  78THEOREM: full DSIC for the single-item second-price auction over the
  79full bid space `ℝ` (not just non-negative bids), and the pivot identity.
  80
  81No HYPOTHESIS, no axiom, no `sorry`.
  82
  83## Scope
  84
  85This file restricts to **single-item** auctions. The general k-item
  86combinatorial VCG follows the same template (allocation = social-welfare
  87maximizer; payment = sum of others' welfare in counterfactual where
  88the bidder is absent), but the combinatorial complexity is not the
  89RS-relevant content here. The single-item case captures the
  90σ-conservation structure that distinguishes VCG from non-VCG mechanisms.
  91-/
  92
  93namespace IndisputableMonolith
  94namespace GameTheory
  95namespace MechanismDesignFromSigma
  96
  97open Constants Cost
  98
  99noncomputable section
 100
 101/-! ## §1. The auction setup -/
 102
 103/-- A bid vector for `n` agents. -/

used by (38)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 8 more

depends on (33)

Lean names referenced from this declaration's body.

… and 3 more