`was`

proved

show as: view math explainer →

module: IndisputableMonolith.GameTheory.MechanismDesignFromSigma
domain: GameTheory
line: 12 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.GameTheory.MechanismDesignFromSigma on GitHub at line 12.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

   9file defined a stub `vcg_sigma_cost` and proved the
  10"truth-telling-is-dominant" lemma only on the trivial branch
  11`others_value = 0`, where every report gave `0 = 0`. The "σ-conservation"
  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
  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:

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.