payment
plain-language theorem explainer
Defines the payment by agent 0 in a two-agent VCG auction: the agent pays the second bid if winning and zero otherwise. Mechanism design researchers cite this rule when establishing dominant-strategy incentive compatibility for single-item auctions. The definition implements the Clarke pivot payment directly via a conditional on the bid comparison.
Claim. For bids $b_0, b_1$, the payment of agent 0 equals $b_1$ if $b_0$ is at least $b_1$ and equals 0 otherwise.
background
The module builds a single-item VCG auction for $n$ agents where each submits a bid $b_i$. The item goes to the highest bidder. The winner pays the highest competing bid while losers pay nothing, exactly the externality imposed on the displaced agent under the Clarke pivot formulation.
proof idea
Direct case definition that returns the second bid on the winning branch and zero on the losing branch. No lemmas are applied.
why it matters
Supplies the concrete payment function needed for the module's dominant-strategy incentive compatibility results, including those for truthful reporting. It realizes the VCG rule inside the sigma-conserving auction construction of track E10.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.