pith. machine review for the scientific record. sign in
theorem proved term proof

dsic_agent_zero

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 147theorem dsic_agent_zero (v₀ b₁ : ℝ) (b₀' : ℝ) :
 148    utility₀ v₀ b₀' b₁ ≤ utility₀ v₀ v₀ b₁ := by

proof body

Term-mode proof.

 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₀`. -/

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.