pivot_identity

formal source

 196/-- **PIVOT IDENTITY.** Under truthful bidding, the winner's payment
 197equals the loser's valuation: the externality the winner imposes on
 198the displaced agent. -/
 199theorem pivot_identity (v₀ v₁ : ℝ) :
 200    -- If agent 0 wins (v₀ ≥ v₁), they pay v₁.
 201    (v₀ ≥ v₁ → payment₀ v₀ v₁ = v₁) ∧
 202    -- If agent 1 wins (v₀ < v₁), they pay v₀.
 203    (v₀ < v₁ → payment₁ v₀ v₁ = v₀) := by
 204  refine ⟨?_, ?_⟩
 205  · intro h
 206    unfold payment₀
 207    rw [if_pos h]
 208  · intro h
 209    unfold payment₁
 210    rw [if_neg (by linarith)]
 211
 212/-- **σ-CONSERVATION (single-item case).** Under truthful bidding, the
 213total surplus on the utility ledger (winner's utility) plus the
 214payment equals the winner's valuation. Equivalently: the auction
 215extracts a payment exactly equal to the social-welfare externality. -/
 216theorem sigma_conservation_truthful (v₀ v₁ : ℝ) :
 217    utility₀ v₀ v₀ v₁ + utility₁ v₁ v₀ v₁ +
 218        (payment₀ v₀ v₁ + payment₁ v₀ v₁)
 219      = max v₀ v₁ := by
 220  unfold utility₀ utility₁ payment₀ payment₁
 221  by_cases h : v₀ ≥ v₁
 222  · -- Agent 0 wins. utility₀ = v₀ - v₁, utility₁ = 0, payment₀ = v₁, payment₁ = 0.
 223    -- Sum = (v₀ - v₁) + 0 + v₁ + 0 = v₀ = max v₀ v₁ (since v₀ ≥ v₁).
 224    rw [if_pos h, if_pos h, if_pos h, if_pos h]
 225    rw [max_eq_left h]
 226    ring
 227  · -- Agent 1 wins. utility₀ = 0, utility₁ = v₁ - v₀, payment₀ = 0, payment₁ = v₀.
 228    -- Sum = 0 + (v₁ - v₀) + 0 + v₀ = v₁ = max v₀ v₁ (since v₁ > v₀).
 229    push_neg at h