winner
plain-language theorem explainer
The allocation selector returns agent 0 when the first bid meets or exceeds the second, otherwise agent 1. Mechanism designers cite it to establish dominant-strategy incentive compatibility in the two-agent VCG setting. The definition is a direct conditional that encodes the highest-bid rule with lowest-index tie resolution.
Claim. For bids $b_0, b_1$ the item is awarded to agent 0 if $b_0$ meets or exceeds $b_1$, and to agent 1 otherwise.
background
The module constructs a single-item VCG auction for two agents indexed in Fin 2. Each agent holds a private valuation and submits a real bid. The allocation rule awards the item to the highest bidder, breaking ties by lowest index. This definition implements that rule exactly. The surrounding development defines payments as the second-highest bid for the winner and zero otherwise, then derives utilities as valuation minus payment when winning.
proof idea
One-line definition that returns the Fin 2 index via a direct comparison of the two bids.
why it matters
The allocation rule supplies the welfare-optimal component required by the DSIC theorems for each agent. Those theorems establish truthful_is_nash and populate the VCGCert structure, confirming dominant-strategy incentive compatibility over the full bid space. The construction advances the sigma-conservation claim for the VCG mechanism in the two-agent case.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.