vcg_payment_eq_sigma_cost

formal source

 277
 278/-- **THE VCG PAYMENT EQUALS THE σ-COST.** Under truthful bidding,
 279the payment by the winner equals the σ-cost of allocating to them. -/
 280theorem vcg_payment_eq_sigma_cost (v₀ v₁ : ℝ) :
 281    -- If agent 0 wins, payment₀ = σ-cost imposed on agent 1.
 282    (v₀ ≥ v₁ → payment₀ v₀ v₁ = sigma_cost_to_agent_0 v₁) ∧
 283    -- If agent 1 wins, payment₁ = σ-cost imposed on agent 0.
 284    (v₀ < v₁ → payment₁ v₀ v₁ = sigma_cost_to_agent_1 v₀) := by
 285  refine ⟨?_, ?_⟩
 286  · intro h
 287    unfold payment₀ sigma_cost_to_agent_0
 288    rw [if_pos h]
 289  · intro h
 290    unfold payment₁ sigma_cost_to_agent_1
 291    rw [if_neg (by linarith)]
 292
 293/-! ## §7. Master certificate -/
 294
 295/-- **VCG MECHANISM DESIGN MASTER CERTIFICATE (Track E10).**
 296
 297Eight clauses, all derived structurally:
 298
 2991. The winner is determined by the higher bid (welfare-optimal allocation).
 3002. DSIC for agent 0 over the full bid space `ℝ`.
 3013. DSIC for agent 1 over the full bid space `ℝ`.
 3024. Truthful bidding is a Nash equilibrium.
 3035. Pivot identity: the winner pays the loser's valuation.
 3046. σ-conservation on the utility ledger under truthful bidding.
 3057. The VCG payment equals the σ-cost the winner imposes on the displaced agent.
 3068. Welfare-optimality of the truthful allocation.
 307
 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. -/