welfare_optimal_truthful
plain-language theorem explainer
The welfare optimality theorem states that the VCG winner rule assigns the item to the agent with the higher valuation. Mechanism designers cite it to confirm that truthful bidding implements the efficient allocation. The short proof performs case analysis on the bid ordering after unfolding the winner definition.
Claim. In the two-agent single-item VCG auction the allocation rule satisfies $(winner(v_0,v_1)=0) ∧ (v_0 ≥ v_1) ∨ (winner(v_0,v_1)=1) ∧ (v_0 < v_1)$, where $winner(b_0,b_1)$ returns $0$ if $b_0 ≥ b_1$ and $1$ otherwise.
background
The module constructs a single-item VCG auction with two agents whose private valuations are $v_0,v_1 ∈ ℝ$. The winner function returns the index of the higher bid, breaking ties toward agent 0. Payments are defined so the winner pays the second-highest bid and losers pay zero; this implements the Clarke pivot rule that charges each winner the externality imposed on the displaced bidder. The surrounding development links the mechanism to σ-conservation by showing that truthful reports preserve the aggregate cost identity across agents.
proof idea
The proof unfolds the winner definition, then splits on the decidable predicate $v_0 ≥ v_1$. The positive case applies the if_pos constructor directly. The negative case pushes the negation, refines the right disjunct, and discharges the remaining if_neg branch with a linarith fact.
why it matters
The result is invoked inside the vcgCert master certificate that packages the DSIC and truthful-Nash lemmas for the σ-conserving auction. It supplies the welfare-maximality step required by the Recognition Science mechanism-design track, ensuring the allocation rule is compatible with the conservation law that descends from the eight-tick octave and the J-cost functional. No open scaffolding remains at this leaf.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.