sigma_conservation_truthful
plain-language theorem explainer
In the two-agent single-item second-price auction, truthful bidding makes the sum of both agents' utilities and both payments equal the winner's valuation. Mechanism designers cite the result as the conservation identity that equates extracted payments to the social-welfare externality. The proof proceeds by case split on which valuation is larger, followed by unfolding the payment and utility definitions and algebraic cancellation.
Claim. For real numbers $v_0, v_1$, the sum of the winner's utility, the loser's utility, and the two payments collected equals $max(v_0, v_1)$ when both agents report their true valuations in the second-price auction.
background
The module defines a single-item VCG auction for two agents. The item is awarded to the higher bidder; the winner pays exactly the loser's bid and the loser pays zero. Utility for an agent equals its valuation minus its payment when it wins and equals zero when it loses. This setup encodes the Clarke pivot rule directly in the payment functions.
proof idea
The proof unfolds the four utility and payment definitions, then splits on whether $v_0$ is at least $v_1$. In the first branch it rewrites the positive conditionals, applies the left-max identity, and cancels with ring. In the second branch it negates the assumption, derives the opposite ordering, rewrites the negated conditionals, applies the right-max identity, and cancels with ring.
why it matters
The theorem supplies the sigma_conservation field inside the VCG certificate, which is then used to assemble the one-statement VCG theorem that simultaneously asserts dominant-strategy incentive compatibility and the pivot identity. It closes the conservation step that links the auction's payment rule to the Recognition framework's sigma-cost accounting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.