VCGCert
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
claimA 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 in Recognition Science
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.
scope and limits
- Does not extend the mechanism to more than two agents.
- Does not treat multi-item or combinatorial auctions.
- Does not incorporate bidder risk preferences or correlated valuations.
- Does not derive the payment rule from the forcing chain T0-T8.
formal statement (Lean)
311structure VCGCert where
312 dsic_zero : ∀ (v₀ b₁ b₀' : ℝ), utility₀ v₀ b₀' b₁ ≤ utility₀ v₀ v₀ b₁
313 dsic_one : ∀ (v₁ b₀ b₁' : ℝ), utility₁ v₁ b₀ b₁' ≤ utility₁ v₁ b₀ v₁
314 truthful_is_nash :
315 ∀ (v₀ v₁ : ℝ),
316 (∀ b₀' : ℝ, utility₀ v₀ b₀' v₁ ≤ utility₀ v₀ v₀ v₁) ∧
317 (∀ b₁' : ℝ, utility₁ v₁ v₀ b₁' ≤ utility₁ v₁ v₀ v₁)
318 pivot_identity :
319 ∀ (v₀ v₁ : ℝ),
320 (v₀ ≥ v₁ → payment₀ v₀ v₁ = v₁) ∧
321 (v₀ < v₁ → payment₁ v₀ v₁ = v₀)
322 sigma_conservation :
323 ∀ (v₀ v₁ : ℝ),
324 utility₀ v₀ v₀ v₁ + utility₁ v₁ v₀ v₁ +
325 (payment₀ v₀ v₁ + payment₁ v₀ v₁) = max v₀ v₁
326 payment_eq_sigma_cost :
327 ∀ (v₀ v₁ : ℝ),
328 (v₀ ≥ v₁ → payment₀ v₀ v₁ = sigma_cost_to_agent_0 v₁) ∧
329 (v₀ < v₁ → payment₁ v₀ v₁ = sigma_cost_to_agent_1 v₀)
330 welfare_optimal :
331 ∀ (v₀ v₁ : ℝ),
332 (winner v₀ v₁ = 0 ∧ v₀ ≥ v₁) ∨ (winner v₀ v₁ = 1 ∧ v₀ < v₁)
333
334/-- The master certificate is inhabited. -/