utility
plain-language theorem explainer
Agent 0's utility in the single-item VCG auction equals their valuation minus the opponent's bid when they win the item and zero when they lose. Mechanism-design researchers cite this payoff function when analyzing dominant-strategy incentive compatibility in the σ-conserving auction. The definition is supplied by a direct case split on the bid comparison.
Claim. For agent 0 with valuation $v_0$ and bids $b_0, b_1$, the utility is $v_0 - b_1$ if $b_0 ≥ b_1$ and equals 0 otherwise.
background
The module constructs a single-item VCG auction with $n ≥ 2$ agents. The allocation awards the item to the highest bidder; the winner pays the second-highest bid while losers pay zero. Agent 0's utility is then valuation minus payment when winning and zero when losing, matching the Clarke pivot rule.
proof idea
Direct definition by case analysis on whether $b_0 ≥ b_1$, implementing the VCG payment rule for the winner.
why it matters
This supplies the payoff function required by the DSIC proofs for each agent in the same module. It realizes the externality-based payment in the σ-conserving auction, closing the gap left by the earlier stub that only handled the trivial zero-valuation case.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.