vcg_one_statement
plain-language theorem explainer
The theorem asserts dominant-strategy incentive compatibility for both agents, the pivot payment identity, and sigma-conservation of total surplus equaling social welfare in the two-agent Vickrey auction. Mechanism designers working inside recognition-based cost frameworks would cite it to connect incentive properties directly to sigma-cost balance. The proof is a one-line term that assembles four supporting lemmas on DSIC and conservation.
Claim. For the single-item second-price auction with two agents having valuations $v_0, v_1$ and bids $b_0, b_1$, the mechanism satisfies: (1) dominant-strategy incentive compatibility, so each agent's utility is maximized by reporting its true valuation for any report of the other; (2) the winner's payment equals the loser's valuation; (3) the sum of both utilities plus payments equals the social welfare value $max(v_0, v_1)$.
background
The module builds a concrete single-item VCG auction for $n$ agents. The allocation rule awards the item to the highest bidder. The payment rule charges the winner the second-highest bid and charges losers zero. Agent utility is then valuation minus payment when winning and zero otherwise. Sigma-cost of an allocation to one agent is defined as the maximum valuation among the remaining agents, representing welfare lost by the displaced runner-up.
proof idea
The proof is a one-line term wrapper that directly packs the dominant-strategy incentive compatibility lemma for the first agent, the corresponding lemma for the second agent, the pivot identity lemma applied under the assumption that the first valuation is at least the second, and the sigma-conservation equality that holds when both agents report truthfully.
why it matters
This declaration completes the core VCG construction in the sigma-conserving auction track by proving incentive compatibility over the unrestricted real bid space and linking payments to sigma-cost. It supplies the explicit four-part statement that replaces earlier trivial stubs. The module note records that the same case analysis extends to $n$ agents by substituting the runner-up bid for the second valuation, leaving the full $n$-agent formalization as the immediate open step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.