vcg_one_statement

formal source

 355    payments equals the winner's valuation = `max v₀ v₁` (social welfare).
 356(4) **Welfare optimality.** The truthful allocation maximizes social
 357    welfare. -/
 358theorem vcg_one_statement :
 359    -- (1) DSIC for agent 0.
 360    (∀ (v₀ b₁ b₀' : ℝ), utility₀ v₀ b₀' b₁ ≤ utility₀ v₀ v₀ b₁) ∧
 361    -- (2) DSIC for agent 1.
 362    (∀ (v₁ b₀ b₁' : ℝ), utility₁ v₁ b₀ b₁' ≤ utility₁ v₁ b₀ v₁) ∧
 363    -- (3) Pivot identity (when 0 wins).
 364    (∀ (v₀ v₁ : ℝ), v₀ ≥ v₁ → payment₀ v₀ v₁ = v₁) ∧
 365    -- (4) σ-conservation under truthful.
 366    (∀ (v₀ v₁ : ℝ),
 367      utility₀ v₀ v₀ v₁ + utility₁ v₁ v₀ v₁ +
 368        (payment₀ v₀ v₁ + payment₁ v₀ v₁) = max v₀ v₁) :=
 369  ⟨dsic_agent_zero, dsic_agent_one,
 370   fun v₀ v₁ h => (pivot_identity v₀ v₁).1 h,
 371   sigma_conservation_truthful⟩
 372
 373end -- noncomputable section
 374
 375/-! ## §9. Note on the n-agent generalization
 376
 377For `n` agents, the same argument applies with the substitutions:
 378
 379- Winner = `argmax b_i`.
 380- Payment by winner = `max_{j ≠ winner} b_j` (the second-highest bid).
 381- σ-cost of allocating to `i` = `max_{j ≠ i} v_j` (welfare lost by displaced runner-up).
 382
 383The DSIC proof generalizes case-by-case (truthful wins/loses ×
 384deviation wins/loses), with the runner-up bid replacing `v₁` / `b₁`
 385in the two-agent argument.
 386
 387Done at `n = 2` here because that is where the σ-conservation
 388structure is cleanest. The combinatorial extension is mechanical