VCGCert
plain-language theorem explainer
VCGCert bundles the eight properties of the two-agent VCG auction derived from sigma conservation: dominant-strategy incentive compatibility for each agent over all real bids, truthful reporting as a Nash equilibrium, the pivot payment rule, sigma conservation on the utility ledger, payments matching imposed sigma costs, and welfare-optimal allocation to the higher valuation. Mechanism designers and Recognition Science researchers on the game-theory track cite this structure to confirm the auction satisfies DSIC without external assumptions. It
Claim. A structure asserting that for valuations $v_0,v_1,b_0',b_1' : ℝ$, agent utilities satisfy $u_0(v_0,b_0',b_1) ≤ u_0(v_0,v_0,b_1)$ and $u_1(v_1,b_0,b_1') ≤ u_1(v_1,b_0,v_1)$ (dominant-strategy incentive compatibility); truthful bids form a Nash equilibrium; the winner pays the loser's valuation (pivot identity); $u_0(v_0,v_0,v_1) + u_1(v_1,v_0,v_1) + (p_0 + p_1) = max(v_0,v_1)$ (sigma conservation); payments equal the sigma costs imposed on the displaced agent; and the item is awarded to the higher valuation (welfare optimality).
background
The module constructs a single-item VCG auction for two agents. Each agent $i$ holds private valuation $v_i ∈ ℝ$ and submits bid $b_i ∈ ℝ$. The item goes to the higher bidder. The winner pays the second-highest bid; losers pay zero. Utility is $v_i - p_i$ if the agent wins and zero otherwise. Sigma cost to agent 0 is defined as $σ-cost_0(v_1) := v_1$, the utility agent 1 forgoes when displaced. The upstream sigma_conservation theorem states: 'The total sigma in a closed system is conserved. If one agent gains sigma, another must lose it.' Pivot identity establishes that truthful payments equal the loser's valuation.
proof idea
VCGCert is a structure definition. Its fields are directly assigned by the supporting lemmas dsic_agent_zero, dsic_agent_one, truthful_is_nash, pivot_identity, sigma_conservation_truthful, and welfare_optimal_truthful. The downstream definition vcgCert assembles these lemmas into an inhabited instance of the structure.
why it matters
VCGCert is instantiated by vcgCert to show the master certificate is inhabited. It completes the VCG mechanism in Track E10, replacing earlier stubs with full DSIC proofs over the real bid space. The structure ties auction payments to the sigma_cost_to_agent_0 definition and the conservation theorem from MoralDebt, ensuring the mechanism respects closed-system sigma accounting. It advances the game-theory track by linking incentives to the sigma ledger and prepares the ground for the n-agent generalization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.