dsic_agent_zero

formal source

 144/-- **DSIC for agent 0.** For any opposing bid `b₁`, agent 0 cannot
 145strictly improve their utility by bidding any `b₀'` other than their
 146true valuation `v₀`. -/
 147theorem dsic_agent_zero (v₀ b₁ : ℝ) (b₀' : ℝ) :
 148    utility₀ v₀ b₀' b₁ ≤ utility₀ v₀ v₀ b₁ := by
 149  unfold utility₀
 150  by_cases h_truth : v₀ ≥ b₁
 151  · -- Truthful: agent 0 wins, utility = v₀ - b₁ ≥ 0.
 152    rw [if_pos h_truth]
 153    by_cases h_dev : b₀' ≥ b₁
 154    · -- Deviation also wins, utility = v₀ - b₁ (same).
 155      rw [if_pos h_dev]
 156    · -- Deviation loses, utility = 0 ≤ v₀ - b₁.
 157      rw [if_neg h_dev]
 158      linarith
 159  · -- Truthful: agent 0 loses, utility = 0.
 160    rw [if_neg h_truth]
 161    by_cases h_dev : b₀' ≥ b₁
 162    · -- Deviation wins, utility = v₀ - b₁ < 0.
 163      rw [if_pos h_dev]
 164      push_neg at h_truth
 165      linarith
 166    · -- Deviation also loses, utility = 0 (same).
 167      rw [if_neg h_dev]
 168
 169/-- **DSIC for agent 1.** Symmetric to agent 0. Note tie-breaking
 170goes to agent 0, so agent 1's wins occur strictly when `b₁ > b₀`. -/
 171theorem dsic_agent_one (v₁ b₀ : ℝ) (b₁' : ℝ) :
 172    utility₁ v₁ b₀ b₁' ≤ utility₁ v₁ b₀ v₁ := by
 173  unfold utility₁
 174  by_cases h_truth : b₀ ≥ v₁
 175  · -- Truthful: agent 1 loses (since b₀ ≥ v₁), utility = 0.
 176    rw [if_pos h_truth]
 177    by_cases h_dev : b₀ ≥ b₁'