VCGCert

formal source

 308This is not a trivial-branch lemma; the DSIC proofs cover all four
 309cases (truthful wins / loses × deviation wins / loses) over the full
 310real bid space. -/
 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. -/
 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