vcgCert

formal source

 332      (winner v₀ v₁ = 0 ∧ v₀ ≥ v₁) ∨ (winner v₀ v₁ = 1 ∧ v₀ < v₁)
 333
 334/-- The master certificate is inhabited. -/
 335def vcgCert : VCGCert where
 336  dsic_zero := dsic_agent_zero
 337  dsic_one := dsic_agent_one
 338  truthful_is_nash := truthful_is_nash
 339  pivot_identity := pivot_identity
 340  sigma_conservation := sigma_conservation_truthful
 341  payment_eq_sigma_cost := vcg_payment_eq_sigma_cost
 342  welfare_optimal := welfare_optimal_truthful
 343
 344/-! ## §8. One-statement summary -/
 345
 346/-- **VCG ONE-STATEMENT THEOREM.**
 347
 348For the single-item second-price auction with two agents:
 349
 350(1) **DSIC.** Truthful reporting is dominant for each agent over the
 351    full bid space `ℝ`.
 352(2) **Pivot identity.** The winner pays the loser's bid (= the
 353    σ-cost the winner imposes on the loser).
 354(3) **σ-conservation.** Total surplus on the utility ledger plus
 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.