dsic_agent_zero
plain-language theorem explainer
In the two-agent second-price auction, agent 0 cannot raise utility by bidding anything other than their true valuation against any fixed opposing bid. Auction theorists cite the result to confirm dominant-strategy incentive compatibility of the Vickrey mechanism. The argument proceeds by exhaustive case analysis on whether the truthful bid wins and whether a deviation wins, with each subcase reduced to an elementary inequality via rewriting and linear arithmetic.
Claim. For all real numbers $v_0, b_1, b_0'$, the utility of an agent with valuation $v_0$ when bidding $b_0'$ against opposing bid $b_1$ is at most the utility obtained by bidding the true valuation $v_0$, where utility equals valuation minus the opposing bid upon winning and zero upon losing.
background
The module constructs a single-item VCG auction for two agents. The item is awarded to the highest bidder (ties broken by lowest index). The winner pays the second-highest bid; losers pay zero. This payment rule implements the Clarke pivot, equaling the externality imposed on the displaced agent. Utility for agent 0 is valuation minus payment if winning and zero otherwise.
proof idea
Unfold the utility definition for agent 0. Split into cases on whether the true valuation meets or exceeds the opposing bid. In each branch perform a further case split on the deviation bid, rewrite the conditional expressions, and close the resulting inequalities with linear arithmetic.
why it matters
The theorem supplies the dominant-strategy incentive compatibility clause for agent 0 in the VCG one-statement theorem. It is invoked to build the master VCG certificate and to prove that truthful bidding forms a Nash equilibrium. In the Recognition Science setting it verifies the incentive properties needed for sigma conservation in the auction mechanism derived from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.